[STATEMENT]
lemma (in Ring) carr_dsum_prod:"carr_dsumag I M \<subseteq> carr_prodag I M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. carr_dsumag I M \<subseteq> carr_prodag I M
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> carr_dsumag I M \<Longrightarrow> x \<in> carr_prodag I M
[PROOF STEP]
apply (simp add:carr_dsumag_def finiteHom_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done