[STATEMENT]
lemma map_family_triangle1:"\<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B;
      bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) (B::'d set); aGroup S;
     \<forall>j\<in>I. ((g j) \<in> aHom S (A j))\<rbrakk> \<Longrightarrow> \<exists>!h. h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and>
                  (\<forall>j\<in>I. compos S (ProjInd I A f j) h =  (g j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j)\<rbrakk> \<Longrightarrow> \<exists>!h. h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) h = g j)
[PROOF STEP]
apply (frule prodag_aGroup[of "I" "A"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A)\<rbrakk> \<Longrightarrow> \<exists>!h. h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) h = g j)
[PROOF STEP]
apply (frule aGroup.Ag_ind_aGroup[of "a\<Pi>\<^bsub>I\<^esub> A" "f" "B"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f)\<rbrakk> \<Longrightarrow> \<exists>!h. h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) h = g j)
[PROOF STEP]
apply (frule Ag_ind_bijec[of "a\<Pi>\<^bsub>I\<^esub> A" "f" "B"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f\<rbrakk> \<Longrightarrow> \<exists>!h. h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) h = g j)
[PROOF STEP]
apply (rule ex_ex1I)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f\<rbrakk> \<Longrightarrow> \<exists>h. h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) h = g j)
 2. \<And>h y. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) h = g j); y \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) y = g j)\<rbrakk> \<Longrightarrow> h = y
[PROOF STEP]
apply (frule map_family_triangle[of "I" "A" "S" "g"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; \<exists>!f. f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j)\<rbrakk> \<Longrightarrow> \<exists>h. h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) h = g j)
 2. \<And>h y. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) h = g j); y \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) y = g j)\<rbrakk> \<Longrightarrow> h = y
[PROOF STEP]
apply (frule ex1_implies_ex)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; \<exists>!f. f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j); \<exists>x. x \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) x = g j)\<rbrakk> \<Longrightarrow> \<exists>h. h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) h = g j)
 2. \<And>h y. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) h = g j); y \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) y = g j)\<rbrakk> \<Longrightarrow> h = y
[PROOF STEP]
apply (erule exE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; \<exists>!f. f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j); x \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) x = g j)\<rbrakk> \<Longrightarrow> \<exists>h. h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) h = g j)
 2. \<And>h y. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) h = g j); y \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) y = g j)\<rbrakk> \<Longrightarrow> h = y
[PROOF STEP]
apply (erule conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; \<exists>!f. f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j); x \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) x = g j\<rbrakk> \<Longrightarrow> \<exists>h. h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) h = g j)
 2. \<And>h y. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) h = g j); y \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) y = g j)\<rbrakk> \<Longrightarrow> h = y
[PROOF STEP]
apply (unfold bijec_def, frule conjunct2, fold bijec_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; \<exists>!f. f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j); x \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) x = g j; surjec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f\<rbrakk> \<Longrightarrow> \<exists>h. h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) h = g j)
 2. \<And>h y. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) h = g j); y \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) y = g j)\<rbrakk> \<Longrightarrow> h = y
[PROOF STEP]
apply (unfold surjec_def, frule conjunct1, fold surjec_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; \<exists>!f. f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j); x \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) x = g j; surjec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; Agii (a\<Pi>\<^bsub>I\<^esub> A) f \<in> aHom (a\<Pi>\<^bsub>I\<^esub> A) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f)\<rbrakk> \<Longrightarrow> \<exists>h. h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) h = g j)
 2. \<And>h y. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) h = g j); y \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) y = g j)\<rbrakk> \<Longrightarrow> h = y
[PROOF STEP]
apply (rename_tac fa,
       frule_tac f = fa in aHom_compos[of "S" "a\<Pi>\<^bsub>I\<^esub> A" "Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f" _
                 "Agii (a\<Pi>\<^bsub>I\<^esub> A) f"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>fa. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; \<exists>!f. f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j); fa \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) fa = g j; surjec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; Agii (a\<Pi>\<^bsub>I\<^esub> A) f \<in> aHom (a\<Pi>\<^bsub>I\<^esub> A) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); compos S (Agii (a\<Pi>\<^bsub>I\<^esub> A) f) fa \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f)\<rbrakk> \<Longrightarrow> \<exists>h. h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) h = g j)
 2. \<And>h y. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) h = g j); y \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) y = g j)\<rbrakk> \<Longrightarrow> h = y
[PROOF STEP]
apply (subgoal_tac "\<forall>j\<in>I. compos S (ProjInd I A f j)
                           (compos S (Agii (a\<Pi>\<^bsub>I\<^esub> A) f) fa) = g j")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>fa. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; \<exists>!f. f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j); fa \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) fa = g j; surjec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; Agii (a\<Pi>\<^bsub>I\<^esub> A) f \<in> aHom (a\<Pi>\<^bsub>I\<^esub> A) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); compos S (Agii (a\<Pi>\<^bsub>I\<^esub> A) f) fa \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. compos S (ProjInd I A f j) (compos S (Agii (a\<Pi>\<^bsub>I\<^esub> A) f) fa) = g j\<rbrakk> \<Longrightarrow> \<exists>h. h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) h = g j)
 2. \<And>fa. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; \<exists>!f. f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j); fa \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) fa = g j; surjec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; Agii (a\<Pi>\<^bsub>I\<^esub> A) f \<in> aHom (a\<Pi>\<^bsub>I\<^esub> A) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); compos S (Agii (a\<Pi>\<^bsub>I\<^esub> A) f) fa \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f)\<rbrakk> \<Longrightarrow> \<forall>j\<in>I. compos S (ProjInd I A f j) (compos S (Agii (a\<Pi>\<^bsub>I\<^esub> A) f) fa) = g j
 3. \<And>h y. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) h = g j); y \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) y = g j)\<rbrakk> \<Longrightarrow> h = y
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>fa. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; \<exists>!f. f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j); fa \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) fa = g j; surjec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; Agii (a\<Pi>\<^bsub>I\<^esub> A) f \<in> aHom (a\<Pi>\<^bsub>I\<^esub> A) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); compos S (Agii (a\<Pi>\<^bsub>I\<^esub> A) f) fa \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f)\<rbrakk> \<Longrightarrow> \<forall>j\<in>I. compos S (ProjInd I A f j) (compos S (Agii (a\<Pi>\<^bsub>I\<^esub> A) f) fa) = g j
 2. \<And>h y. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) h = g j); y \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) y = g j)\<rbrakk> \<Longrightarrow> h = y
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>fa j. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; \<exists>!f. f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j); fa \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) fa = g j; surjec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; Agii (a\<Pi>\<^bsub>I\<^esub> A) f \<in> aHom (a\<Pi>\<^bsub>I\<^esub> A) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); compos S (Agii (a\<Pi>\<^bsub>I\<^esub> A) f) fa \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); j \<in> I\<rbrakk> \<Longrightarrow> compos S (ProjInd I A f j) (compos S (Agii (a\<Pi>\<^bsub>I\<^esub> A) f) fa) = g j
 2. \<And>h y. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) h = g j); y \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) y = g j)\<rbrakk> \<Longrightarrow> h = y
[PROOF STEP]
apply (frule_tac N = "A j" and f = fa and g = "Agii (a\<Pi>\<^bsub>I\<^esub> A) f" and
 h = "ProjInd I A f j" in aHom_compos_assoc[of "S" "a\<Pi>\<^bsub>I\<^esub> A" "Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f"],
 assumption+)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>fa j. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; \<exists>!f. f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j); fa \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) fa = g j; surjec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; Agii (a\<Pi>\<^bsub>I\<^esub> A) f \<in> aHom (a\<Pi>\<^bsub>I\<^esub> A) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); compos S (Agii (a\<Pi>\<^bsub>I\<^esub> A) f) fa \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); j \<in> I\<rbrakk> \<Longrightarrow> aGroup (A j)
 2. \<And>fa j. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; \<exists>!f. f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j); fa \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) fa = g j; surjec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; Agii (a\<Pi>\<^bsub>I\<^esub> A) f \<in> aHom (a\<Pi>\<^bsub>I\<^esub> A) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); compos S (Agii (a\<Pi>\<^bsub>I\<^esub> A) f) fa \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); j \<in> I\<rbrakk> \<Longrightarrow> fa \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A)
 3. \<And>fa j. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; \<exists>!f. f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j); fa \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) fa = g j; surjec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; Agii (a\<Pi>\<^bsub>I\<^esub> A) f \<in> aHom (a\<Pi>\<^bsub>I\<^esub> A) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); compos S (Agii (a\<Pi>\<^bsub>I\<^esub> A) f) fa \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); j \<in> I\<rbrakk> \<Longrightarrow> Agii (a\<Pi>\<^bsub>I\<^esub> A) f \<in> aHom (a\<Pi>\<^bsub>I\<^esub> A) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f)
 4. \<And>fa j. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; \<exists>!f. f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j); fa \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) fa = g j; surjec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; Agii (a\<Pi>\<^bsub>I\<^esub> A) f \<in> aHom (a\<Pi>\<^bsub>I\<^esub> A) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); compos S (Agii (a\<Pi>\<^bsub>I\<^esub> A) f) fa \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); j \<in> I\<rbrakk> \<Longrightarrow> ProjInd I A f j \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (A j)
 5. \<And>fa j. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; \<exists>!f. f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j); fa \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) fa = g j; surjec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; Agii (a\<Pi>\<^bsub>I\<^esub> A) f \<in> aHom (a\<Pi>\<^bsub>I\<^esub> A) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); compos S (Agii (a\<Pi>\<^bsub>I\<^esub> A) f) fa \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); j \<in> I; compos S (ProjInd I A f j) (compos S (Agii (a\<Pi>\<^bsub>I\<^esub> A) f) fa) = compos S (compos (a\<Pi>\<^bsub>I\<^esub> A) (ProjInd I A f j) (Agii (a\<Pi>\<^bsub>I\<^esub> A) f)) fa\<rbrakk> \<Longrightarrow> compos S (ProjInd I A f j) (compos S (Agii (a\<Pi>\<^bsub>I\<^esub> A) f) fa) = g j
 6. \<And>h y. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) h = g j); y \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) y = g j)\<rbrakk> \<Longrightarrow> h = y
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>fa j. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; \<exists>!f. f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j); fa \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) fa = g j; surjec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; Agii (a\<Pi>\<^bsub>I\<^esub> A) f \<in> aHom (a\<Pi>\<^bsub>I\<^esub> A) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); compos S (Agii (a\<Pi>\<^bsub>I\<^esub> A) f) fa \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); j \<in> I\<rbrakk> \<Longrightarrow> fa \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A)
 2. \<And>fa j. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; \<exists>!f. f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j); fa \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) fa = g j; surjec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; Agii (a\<Pi>\<^bsub>I\<^esub> A) f \<in> aHom (a\<Pi>\<^bsub>I\<^esub> A) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); compos S (Agii (a\<Pi>\<^bsub>I\<^esub> A) f) fa \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); j \<in> I\<rbrakk> \<Longrightarrow> Agii (a\<Pi>\<^bsub>I\<^esub> A) f \<in> aHom (a\<Pi>\<^bsub>I\<^esub> A) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f)
 3. \<And>fa j. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; \<exists>!f. f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j); fa \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) fa = g j; surjec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; Agii (a\<Pi>\<^bsub>I\<^esub> A) f \<in> aHom (a\<Pi>\<^bsub>I\<^esub> A) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); compos S (Agii (a\<Pi>\<^bsub>I\<^esub> A) f) fa \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); j \<in> I\<rbrakk> \<Longrightarrow> ProjInd I A f j \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (A j)
 4. \<And>fa j. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; \<exists>!f. f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j); fa \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) fa = g j; surjec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; Agii (a\<Pi>\<^bsub>I\<^esub> A) f \<in> aHom (a\<Pi>\<^bsub>I\<^esub> A) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); compos S (Agii (a\<Pi>\<^bsub>I\<^esub> A) f) fa \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); j \<in> I; compos S (ProjInd I A f j) (compos S (Agii (a\<Pi>\<^bsub>I\<^esub> A) f) fa) = compos S (compos (a\<Pi>\<^bsub>I\<^esub> A) (ProjInd I A f j) (Agii (a\<Pi>\<^bsub>I\<^esub> A) f)) fa\<rbrakk> \<Longrightarrow> compos S (ProjInd I A f j) (compos S (Agii (a\<Pi>\<^bsub>I\<^esub> A) f) fa) = g j
 5. \<And>h y. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) h = g j); y \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) y = g j)\<rbrakk> \<Longrightarrow> h = y
[PROOF STEP]
apply assumption+
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>fa j. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; \<exists>!f. f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j); fa \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) fa = g j; surjec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; Agii (a\<Pi>\<^bsub>I\<^esub> A) f \<in> aHom (a\<Pi>\<^bsub>I\<^esub> A) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); compos S (Agii (a\<Pi>\<^bsub>I\<^esub> A) f) fa \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); j \<in> I\<rbrakk> \<Longrightarrow> ProjInd I A f j \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (A j)
 2. \<And>fa j. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; \<exists>!f. f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j); fa \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) fa = g j; surjec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; Agii (a\<Pi>\<^bsub>I\<^esub> A) f \<in> aHom (a\<Pi>\<^bsub>I\<^esub> A) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); compos S (Agii (a\<Pi>\<^bsub>I\<^esub> A) f) fa \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); j \<in> I; compos S (ProjInd I A f j) (compos S (Agii (a\<Pi>\<^bsub>I\<^esub> A) f) fa) = compos S (compos (a\<Pi>\<^bsub>I\<^esub> A) (ProjInd I A f j) (Agii (a\<Pi>\<^bsub>I\<^esub> A) f)) fa\<rbrakk> \<Longrightarrow> compos S (ProjInd I A f j) (compos S (Agii (a\<Pi>\<^bsub>I\<^esub> A) f) fa) = g j
 3. \<And>h y. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) h = g j); y \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) y = g j)\<rbrakk> \<Longrightarrow> h = y
[PROOF STEP]
apply (simp add:ProjInd_aHom)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>fa j. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; \<exists>!f. f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j); fa \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) fa = g j; surjec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; Agii (a\<Pi>\<^bsub>I\<^esub> A) f \<in> aHom (a\<Pi>\<^bsub>I\<^esub> A) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); compos S (Agii (a\<Pi>\<^bsub>I\<^esub> A) f) fa \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); j \<in> I; compos S (ProjInd I A f j) (compos S (Agii (a\<Pi>\<^bsub>I\<^esub> A) f) fa) = compos S (compos (a\<Pi>\<^bsub>I\<^esub> A) (ProjInd I A f j) (Agii (a\<Pi>\<^bsub>I\<^esub> A) f)) fa\<rbrakk> \<Longrightarrow> compos S (ProjInd I A f j) (compos S (Agii (a\<Pi>\<^bsub>I\<^esub> A) f) fa) = g j
 2. \<And>h y. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) h = g j); y \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) y = g j)\<rbrakk> \<Longrightarrow> h = y
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>fa j. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; \<exists>!f. f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j); fa \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) fa = g j; surjec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; Agii (a\<Pi>\<^bsub>I\<^esub> A) f \<in> aHom (a\<Pi>\<^bsub>I\<^esub> A) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); compos S (Agii (a\<Pi>\<^bsub>I\<^esub> A) f) fa \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); j \<in> I; compos S (ProjInd I A f j) (compos S (Agii (a\<Pi>\<^bsub>I\<^esub> A) f) fa) = compos S (compos (a\<Pi>\<^bsub>I\<^esub> A) (ProjInd I A f j) (Agii (a\<Pi>\<^bsub>I\<^esub> A) f)) fa\<rbrakk> \<Longrightarrow> compos S (compos (a\<Pi>\<^bsub>I\<^esub> A) (ProjInd I A f j) (Agii (a\<Pi>\<^bsub>I\<^esub> A) f)) fa = g j
 2. \<And>h y. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) h = g j); y \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) y = g j)\<rbrakk> \<Longrightarrow> h = y
[PROOF STEP]
apply (thin_tac "compos S (ProjInd I A f j) (compos S (Agii (a\<Pi>\<^bsub>I\<^esub> A) f) fa) =
        compos S (compos (a\<Pi>\<^bsub>I\<^esub> A) (ProjInd I A f j) (Agii (a\<Pi>\<^bsub>I\<^esub> A) f)) fa")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>fa j. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; \<exists>!f. f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j); fa \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) fa = g j; surjec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; Agii (a\<Pi>\<^bsub>I\<^esub> A) f \<in> aHom (a\<Pi>\<^bsub>I\<^esub> A) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); compos S (Agii (a\<Pi>\<^bsub>I\<^esub> A) f) fa \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); j \<in> I\<rbrakk> \<Longrightarrow> compos S (compos (a\<Pi>\<^bsub>I\<^esub> A) (ProjInd I A f j) (Agii (a\<Pi>\<^bsub>I\<^esub> A) f)) fa = g j
 2. \<And>h y. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) h = g j); y \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) y = g j)\<rbrakk> \<Longrightarrow> h = y
[PROOF STEP]
apply (simp add:Ag_ind_triangle1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h y. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) h = g j); y \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) y = g j)\<rbrakk> \<Longrightarrow> h = y
[PROOF STEP]
apply (rename_tac h h1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h h1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) h = g j); h1 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<and> (\<forall>j\<in>I. compos S (ProjInd I A f j) h1 = g j)\<rbrakk> \<Longrightarrow> h = h1
[PROOF STEP]
apply (erule conjE)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h h1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. compos S (ProjInd I A f j) h = g j; h1 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. compos S (ProjInd I A f j) h1 = g j\<rbrakk> \<Longrightarrow> h = h1
[PROOF STEP]
apply (rule funcset_eq[of _ "carrier S"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>h h1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. compos S (ProjInd I A f j) h = g j; h1 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. compos S (ProjInd I A f j) h1 = g j\<rbrakk> \<Longrightarrow> h \<in> extensional (carrier S)
 2. \<And>h h1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. compos S (ProjInd I A f j) h = g j; h1 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. compos S (ProjInd I A f j) h1 = g j\<rbrakk> \<Longrightarrow> h1 \<in> extensional (carrier S)
 3. \<And>h h1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. compos S (ProjInd I A f j) h = g j; h1 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. compos S (ProjInd I A f j) h1 = g j\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier S. h x = h1 x
[PROOF STEP]
apply (simp add:aHom_def, simp add:aHom_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h h1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. compos S (ProjInd I A f j) h = g j; h1 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. compos S (ProjInd I A f j) h1 = g j\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier S. h x = h1 x
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h h1 x. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. compos S (ProjInd I A f j) h = g j; h1 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. compos S (ProjInd I A f j) h1 = g j; x \<in> carrier S\<rbrakk> \<Longrightarrow> h x = h1 x
[PROOF STEP]
apply (simp add:compos_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h h1 x. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. compose (carrier S) (ProjInd I A f j) h = g j; h1 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. compose (carrier S) (ProjInd I A f j) h1 = g j; x \<in> carrier S\<rbrakk> \<Longrightarrow> h x = h1 x
[PROOF STEP]
apply (frule_tac f = h and a = x in aHom_mem[of "S" "Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f"],
          assumption+,
       frule_tac f = h1 and a = x in aHom_mem[of "S" "Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f"],
          assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h h1 x. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. compose (carrier S) (ProjInd I A f j) h = g j; h1 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. compose (carrier S) (ProjInd I A f j) h1 = g j; x \<in> carrier S; h x \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); h1 x \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f)\<rbrakk> \<Longrightarrow> h x = h1 x
[PROOF STEP]
apply (rule_tac x = "h x" and y = "h1 x" in ProjInd_mem_eq[of "I" "A" "f"
       "B" "S"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h h1 x. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. compose (carrier S) (ProjInd I A f j) h = g j; h1 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. compose (carrier S) (ProjInd I A f j) h1 = g j; x \<in> carrier S; h x \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); h1 x \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f)\<rbrakk> \<Longrightarrow> \<forall>j\<in>I. ProjInd I A f j (h x) = ProjInd I A f j (h1 x)
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h h1 x j. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. compose (carrier S) (ProjInd I A f j) h = g j; h1 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. compose (carrier S) (ProjInd I A f j) h1 = g j; x \<in> carrier S; h x \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); h1 x \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); j \<in> I\<rbrakk> \<Longrightarrow> ProjInd I A f j (h x) = ProjInd I A f j (h1 x)
[PROOF STEP]
apply (rotate_tac 5,
       frule_tac x = j in bspec, assumption,
       thin_tac "\<forall>j\<in>I. compose (carrier S) (ProjInd I A f j) h = g j",
       frule_tac x = j in bspec, assumption,
       thin_tac "\<forall>j\<in>I. compose (carrier S) (ProjInd I A f j) h1 = g j")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h h1 x j. \<lbrakk>aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) f; h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); h1 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); x \<in> carrier S; h x \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); h1 x \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); j \<in> I; \<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); compose (carrier S) (ProjInd I A f j) h = g j; compose (carrier S) (ProjInd I A f j) h1 = g j\<rbrakk> \<Longrightarrow> ProjInd I A f j (h x) = ProjInd I A f j (h1 x)
[PROOF STEP]
apply (simp add:compose_def,
       subgoal_tac "(\<lambda>x\<in>carrier S. ProjInd I A f j (h x)) x = g j x",
       thin_tac "(\<lambda>x\<in>carrier S. ProjInd I A f j (h x)) = g j",
       subgoal_tac "(\<lambda>x\<in>carrier S. ProjInd I A f j (h1 x)) x = g j x",
       thin_tac "(\<lambda>x\<in>carrier S. ProjInd I A f j (h1 x)) = g j", simp+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma  map_family_triangle2:"\<lbrakk>I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S;
       \<forall>j\<in>I. g j \<in> aHom S (A j); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B;
        bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B;
        h1 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S;
        \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (g j) h1 = ProjInd I A ff j;
        h2 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff);
        \<forall>j\<in>I. compos S (ProjInd I A ff j) h2 = g j\<rbrakk>
       \<Longrightarrow> \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (ProjInd I A ff j)
                 (compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) h2 h1) =
                ProjInd I A ff j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; h1 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S; \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (g j) h1 = ProjInd I A ff j; h2 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); \<forall>j\<in>I. compos S (ProjInd I A ff j) h2 = g j\<rbrakk> \<Longrightarrow> \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (ProjInd I A ff j) (compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) h2 h1) = ProjInd I A ff j
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; h1 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S; \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (g j) h1 = ProjInd I A ff j; h2 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); \<forall>j\<in>I. compos S (ProjInd I A ff j) h2 = g j; j \<in> I\<rbrakk> \<Longrightarrow> compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (ProjInd I A ff j) (compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) h2 h1) = ProjInd I A ff j
[PROOF STEP]
apply (frule prodag_aGroup[of "I" "A"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; h1 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S; \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (g j) h1 = ProjInd I A ff j; h2 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); \<forall>j\<in>I. compos S (ProjInd I A ff j) h2 = g j; j \<in> I; aGroup (a\<Pi>\<^bsub>I\<^esub> A)\<rbrakk> \<Longrightarrow> compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (ProjInd I A ff j) (compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) h2 h1) = ProjInd I A ff j
[PROOF STEP]
apply (frule_tac f = ff in aGroup.Ag_ind_aGroup[of "a\<Pi>\<^bsub>I\<^esub> A" _ "B"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; h1 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S; \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (g j) h1 = ProjInd I A ff j; h2 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); \<forall>j\<in>I. compos S (ProjInd I A ff j) h2 = g j; j \<in> I; aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff)\<rbrakk> \<Longrightarrow> compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (ProjInd I A ff j) (compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) h2 h1) = ProjInd I A ff j
[PROOF STEP]
apply (frule_tac N = "A j" and h = "ProjInd I A ff j" in aHom_compos_assoc[of "Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff" "S" "Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff" _ "h1" "h2"], assumption+)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>j. \<lbrakk>I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; h1 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S; \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (g j) h1 = ProjInd I A ff j; h2 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); \<forall>j\<in>I. compos S (ProjInd I A ff j) h2 = g j; j \<in> I; aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff)\<rbrakk> \<Longrightarrow> aGroup (A j)
 2. \<And>j. \<lbrakk>I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; h1 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S; \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (g j) h1 = ProjInd I A ff j; h2 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); \<forall>j\<in>I. compos S (ProjInd I A ff j) h2 = g j; j \<in> I; aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff)\<rbrakk> \<Longrightarrow> h1 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S
 3. \<And>j. \<lbrakk>I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; h1 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S; \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (g j) h1 = ProjInd I A ff j; h2 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); \<forall>j\<in>I. compos S (ProjInd I A ff j) h2 = g j; j \<in> I; aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff)\<rbrakk> \<Longrightarrow> h2 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff)
 4. \<And>j. \<lbrakk>I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; h1 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S; \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (g j) h1 = ProjInd I A ff j; h2 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); \<forall>j\<in>I. compos S (ProjInd I A ff j) h2 = g j; j \<in> I; aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff)\<rbrakk> \<Longrightarrow> ProjInd I A ff j \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (A j)
 5. \<And>j. \<lbrakk>I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; h1 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S; \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (g j) h1 = ProjInd I A ff j; h2 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); \<forall>j\<in>I. compos S (ProjInd I A ff j) h2 = g j; j \<in> I; aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (ProjInd I A ff j) (compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) h2 h1) = compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (compos S (ProjInd I A ff j) h2) h1\<rbrakk> \<Longrightarrow> compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (ProjInd I A ff j) (compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) h2 h1) = ProjInd I A ff j
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>j. \<lbrakk>I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; h1 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S; \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (g j) h1 = ProjInd I A ff j; h2 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); \<forall>j\<in>I. compos S (ProjInd I A ff j) h2 = g j; j \<in> I; aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff)\<rbrakk> \<Longrightarrow> h1 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S
 2. \<And>j. \<lbrakk>I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; h1 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S; \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (g j) h1 = ProjInd I A ff j; h2 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); \<forall>j\<in>I. compos S (ProjInd I A ff j) h2 = g j; j \<in> I; aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff)\<rbrakk> \<Longrightarrow> h2 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff)
 3. \<And>j. \<lbrakk>I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; h1 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S; \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (g j) h1 = ProjInd I A ff j; h2 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); \<forall>j\<in>I. compos S (ProjInd I A ff j) h2 = g j; j \<in> I; aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff)\<rbrakk> \<Longrightarrow> ProjInd I A ff j \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (A j)
 4. \<And>j. \<lbrakk>I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; h1 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S; \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (g j) h1 = ProjInd I A ff j; h2 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); \<forall>j\<in>I. compos S (ProjInd I A ff j) h2 = g j; j \<in> I; aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (ProjInd I A ff j) (compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) h2 h1) = compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (compos S (ProjInd I A ff j) h2) h1\<rbrakk> \<Longrightarrow> compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (ProjInd I A ff j) (compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) h2 h1) = ProjInd I A ff j
[PROOF STEP]
apply assumption+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; h1 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S; \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (g j) h1 = ProjInd I A ff j; h2 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); \<forall>j\<in>I. compos S (ProjInd I A ff j) h2 = g j; j \<in> I; aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff)\<rbrakk> \<Longrightarrow> ProjInd I A ff j \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (A j)
 2. \<And>j. \<lbrakk>I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; h1 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S; \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (g j) h1 = ProjInd I A ff j; h2 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); \<forall>j\<in>I. compos S (ProjInd I A ff j) h2 = g j; j \<in> I; aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (ProjInd I A ff j) (compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) h2 h1) = compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (compos S (ProjInd I A ff j) h2) h1\<rbrakk> \<Longrightarrow> compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (ProjInd I A ff j) (compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) h2 h1) = ProjInd I A ff j
[PROOF STEP]
apply (simp add:ProjInd_aHom)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; h1 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S; \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (g j) h1 = ProjInd I A ff j; h2 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); \<forall>j\<in>I. compos S (ProjInd I A ff j) h2 = g j; j \<in> I; aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (ProjInd I A ff j) (compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) h2 h1) = compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (compos S (ProjInd I A ff j) h2) h1\<rbrakk> \<Longrightarrow> compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (ProjInd I A ff j) (compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) h2 h1) = ProjInd I A ff j
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma  map_family_triangle3:"\<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; aGroup S1;
       \<forall>j\<in>I. f j \<in> aHom S (A j); \<forall>j\<in>I. g j \<in> aHom S1 (A j);
        h1 \<in> aHom S1 S; h2 \<in> aHom S S1;
        \<forall>j\<in>I. compos S (g j) h2 = f j;
        \<forall>j\<in>I. compos S1 (f j) h1 = g j\<rbrakk>
       \<Longrightarrow> \<forall>j\<in>I. compos S (f j) (compos S h1 h2) = f j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; aGroup S1; \<forall>j\<in>I. f j \<in> aHom S (A j); \<forall>j\<in>I. g j \<in> aHom S1 (A j); h1 \<in> aHom S1 S; h2 \<in> aHom S S1; \<forall>j\<in>I. compos S (g j) h2 = f j; \<forall>j\<in>I. compos S1 (f j) h1 = g j\<rbrakk> \<Longrightarrow> \<forall>j\<in>I. compos S (f j) (compos S h1 h2) = f j
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; aGroup S1; \<forall>j\<in>I. f j \<in> aHom S (A j); \<forall>j\<in>I. g j \<in> aHom S1 (A j); h1 \<in> aHom S1 S; h2 \<in> aHom S S1; \<forall>j\<in>I. compos S (g j) h2 = f j; \<forall>j\<in>I. compos S1 (f j) h1 = g j; j \<in> I\<rbrakk> \<Longrightarrow> compos S (f j) (compos S h1 h2) = f j
[PROOF STEP]
apply (frule_tac h = "f j" and N = "A j" in aHom_compos_assoc[of "S" "S1"
                              "S" _ "h2" "h1"], assumption+)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>j. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; aGroup S1; \<forall>j\<in>I. f j \<in> aHom S (A j); \<forall>j\<in>I. g j \<in> aHom S1 (A j); h1 \<in> aHom S1 S; h2 \<in> aHom S S1; \<forall>j\<in>I. compos S (g j) h2 = f j; \<forall>j\<in>I. compos S1 (f j) h1 = g j; j \<in> I\<rbrakk> \<Longrightarrow> aGroup (A j)
 2. \<And>j. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; aGroup S1; \<forall>j\<in>I. f j \<in> aHom S (A j); \<forall>j\<in>I. g j \<in> aHom S1 (A j); h1 \<in> aHom S1 S; h2 \<in> aHom S S1; \<forall>j\<in>I. compos S (g j) h2 = f j; \<forall>j\<in>I. compos S1 (f j) h1 = g j; j \<in> I\<rbrakk> \<Longrightarrow> h2 \<in> aHom S S1
 3. \<And>j. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; aGroup S1; \<forall>j\<in>I. f j \<in> aHom S (A j); \<forall>j\<in>I. g j \<in> aHom S1 (A j); h1 \<in> aHom S1 S; h2 \<in> aHom S S1; \<forall>j\<in>I. compos S (g j) h2 = f j; \<forall>j\<in>I. compos S1 (f j) h1 = g j; j \<in> I\<rbrakk> \<Longrightarrow> h1 \<in> aHom S1 S
 4. \<And>j. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; aGroup S1; \<forall>j\<in>I. f j \<in> aHom S (A j); \<forall>j\<in>I. g j \<in> aHom S1 (A j); h1 \<in> aHom S1 S; h2 \<in> aHom S S1; \<forall>j\<in>I. compos S (g j) h2 = f j; \<forall>j\<in>I. compos S1 (f j) h1 = g j; j \<in> I\<rbrakk> \<Longrightarrow> f j \<in> aHom S (A j)
 5. \<And>j. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; aGroup S1; \<forall>j\<in>I. f j \<in> aHom S (A j); \<forall>j\<in>I. g j \<in> aHom S1 (A j); h1 \<in> aHom S1 S; h2 \<in> aHom S S1; \<forall>j\<in>I. compos S (g j) h2 = f j; \<forall>j\<in>I. compos S1 (f j) h1 = g j; j \<in> I; compos S (f j) (compos S h1 h2) = compos S (compos S1 (f j) h1) h2\<rbrakk> \<Longrightarrow> compos S (f j) (compos S h1 h2) = f j
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>j. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; aGroup S1; \<forall>j\<in>I. f j \<in> aHom S (A j); \<forall>j\<in>I. g j \<in> aHom S1 (A j); h1 \<in> aHom S1 S; h2 \<in> aHom S S1; \<forall>j\<in>I. compos S (g j) h2 = f j; \<forall>j\<in>I. compos S1 (f j) h1 = g j; j \<in> I\<rbrakk> \<Longrightarrow> h2 \<in> aHom S S1
 2. \<And>j. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; aGroup S1; \<forall>j\<in>I. f j \<in> aHom S (A j); \<forall>j\<in>I. g j \<in> aHom S1 (A j); h1 \<in> aHom S1 S; h2 \<in> aHom S S1; \<forall>j\<in>I. compos S (g j) h2 = f j; \<forall>j\<in>I. compos S1 (f j) h1 = g j; j \<in> I\<rbrakk> \<Longrightarrow> h1 \<in> aHom S1 S
 3. \<And>j. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; aGroup S1; \<forall>j\<in>I. f j \<in> aHom S (A j); \<forall>j\<in>I. g j \<in> aHom S1 (A j); h1 \<in> aHom S1 S; h2 \<in> aHom S S1; \<forall>j\<in>I. compos S (g j) h2 = f j; \<forall>j\<in>I. compos S1 (f j) h1 = g j; j \<in> I\<rbrakk> \<Longrightarrow> f j \<in> aHom S (A j)
 4. \<And>j. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; aGroup S1; \<forall>j\<in>I. f j \<in> aHom S (A j); \<forall>j\<in>I. g j \<in> aHom S1 (A j); h1 \<in> aHom S1 S; h2 \<in> aHom S S1; \<forall>j\<in>I. compos S (g j) h2 = f j; \<forall>j\<in>I. compos S1 (f j) h1 = g j; j \<in> I; compos S (f j) (compos S h1 h2) = compos S (compos S1 (f j) h1) h2\<rbrakk> \<Longrightarrow> compos S (f j) (compos S h1 h2) = f j
[PROOF STEP]
apply assumption+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; aGroup S1; \<forall>j\<in>I. f j \<in> aHom S (A j); \<forall>j\<in>I. g j \<in> aHom S1 (A j); h1 \<in> aHom S1 S; h2 \<in> aHom S S1; \<forall>j\<in>I. compos S (g j) h2 = f j; \<forall>j\<in>I. compos S1 (f j) h1 = g j; j \<in> I\<rbrakk> \<Longrightarrow> f j \<in> aHom S (A j)
 2. \<And>j. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; aGroup S1; \<forall>j\<in>I. f j \<in> aHom S (A j); \<forall>j\<in>I. g j \<in> aHom S1 (A j); h1 \<in> aHom S1 S; h2 \<in> aHom S S1; \<forall>j\<in>I. compos S (g j) h2 = f j; \<forall>j\<in>I. compos S1 (f j) h1 = g j; j \<in> I; compos S (f j) (compos S h1 h2) = compos S (compos S1 (f j) h1) h2\<rbrakk> \<Longrightarrow> compos S (f j) (compos S h1 h2) = f j
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; aGroup S1; \<forall>j\<in>I. f j \<in> aHom S (A j); \<forall>j\<in>I. g j \<in> aHom S1 (A j); h1 \<in> aHom S1 S; h2 \<in> aHom S S1; \<forall>j\<in>I. compos S (g j) h2 = f j; \<forall>j\<in>I. compos S1 (f j) h1 = g j; j \<in> I; compos S (f j) (compos S h1 h2) = compos S (compos S1 (f j) h1) h2\<rbrakk> \<Longrightarrow> compos S (f j) (compos S h1 h2) = f j
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma map_family_triangle4:"\<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S;
                \<forall>j\<in>I. f j \<in> aHom S (A j)\<rbrakk> \<Longrightarrow>
               \<forall>j\<in>I. compos S (f j) (ag_idmap S) = f j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. f j \<in> aHom S (A j)\<rbrakk> \<Longrightarrow> \<forall>j\<in>I. compos S (f j) aI\<^bsub>S\<^esub> = f j
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. f j \<in> aHom S (A j); j \<in> I\<rbrakk> \<Longrightarrow> compos S (f j) aI\<^bsub>S\<^esub> = f j
[PROOF STEP]
apply (frule_tac x = j in bspec, assumption,
       thin_tac "\<forall>j\<in>I. aGroup (A j)",
       frule_tac x = j in bspec, assumption,
       thin_tac "\<forall>j\<in>I. f j \<in> aHom S (A j)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>aGroup S; j \<in> I; aGroup (A j); f j \<in> aHom S (A j)\<rbrakk> \<Longrightarrow> compos S (f j) aI\<^bsub>S\<^esub> = f j
[PROOF STEP]
apply (simp add:compos_aI_r)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma  prod_triangle:"\<lbrakk>I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S;
       \<forall>j\<in>I. g j \<in> aHom S (A j); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B;
        bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B;
        h1 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S;
        \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (g j) h1 = ProjInd I A ff j;
        h2 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff);
        \<forall>j\<in>I. compos S (ProjInd I A ff j) h2 = g j\<rbrakk>
       \<Longrightarrow> (compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) h2 h1) = ag_idmap (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; h1 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S; \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (g j) h1 = ProjInd I A ff j; h2 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); \<forall>j\<in>I. compos S (ProjInd I A ff j) h2 = g j\<rbrakk> \<Longrightarrow> compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) h2 h1 = aI\<^bsub>Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff\<^esub>
[PROOF STEP]
apply (frule map_family_triangle2[of "I" "A" "S" "g" "ff" "B" "h1" "h2"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; h1 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S; \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (g j) h1 = ProjInd I A ff j; h2 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); \<forall>j\<in>I. compos S (ProjInd I A ff j) h2 = g j; \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (ProjInd I A ff j) (compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) h2 h1) = ProjInd I A ff j\<rbrakk> \<Longrightarrow> compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) h2 h1 = aI\<^bsub>Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff\<^esub>
[PROOF STEP]
apply (frule prodag_aGroup[of "I" "A"],
       frule aGroup.Ag_ind_aGroup[of "a\<Pi>\<^bsub>I\<^esub> A" "ff" "B"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; h1 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S; \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (g j) h1 = ProjInd I A ff j; h2 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); \<forall>j\<in>I. compos S (ProjInd I A ff j) h2 = g j; \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (ProjInd I A ff j) (compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) h2 h1) = ProjInd I A ff j; aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff)\<rbrakk> \<Longrightarrow> compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) h2 h1 = aI\<^bsub>Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff\<^esub>
[PROOF STEP]
apply (frule aHom_compos[of "Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff" "S" "Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff" "h1"
                            "h2"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; h1 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S; \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (g j) h1 = ProjInd I A ff j; h2 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); \<forall>j\<in>I. compos S (ProjInd I A ff j) h2 = g j; \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (ProjInd I A ff j) (compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) h2 h1) = ProjInd I A ff j; aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) h2 h1 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff)\<rbrakk> \<Longrightarrow> compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) h2 h1 = aI\<^bsub>Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff\<^esub>
[PROOF STEP]
apply (rule ProjInd_mem_eq1[of "I" "A" "ff" "B" "S"
                            "compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) h2 h1"], assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done