[STATEMENT]
lemma Ag_ind_triangle:"\<lbrakk>\<forall>j\<in>I. aGroup (A j); j \<in> I; f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B;
      bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) (B::'d set); j \<in> I\<rbrakk> \<Longrightarrow>
compos (a\<Pi>\<^bsub>I\<^esub> A) (compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f)(PRoject I A j) (ainvf\<^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) =
                                       PRoject I A j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); j \<in> I; f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; j \<in> I\<rbrakk> \<Longrightarrow> compos (a\<Pi>\<^bsub>I\<^esub> A) (compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (\<pi>\<^bsub>I,A,j\<^esub>) (ainvf\<^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) = \<pi>\<^bsub>I,A,j\<^esub>
[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); j \<in> I; f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; j \<in> I; aGroup (a\<Pi>\<^bsub>I\<^esub> A)\<rbrakk> \<Longrightarrow> compos (a\<Pi>\<^bsub>I\<^esub> A) (compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (\<pi>\<^bsub>I,A,j\<^esub>) (ainvf\<^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) = \<pi>\<^bsub>I,A,j\<^esub>
[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); j \<in> I; f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; j \<in> I; aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f)\<rbrakk> \<Longrightarrow> compos (a\<Pi>\<^bsub>I\<^esub> A) (compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (\<pi>\<^bsub>I,A,j\<^esub>) (ainvf\<^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) = \<pi>\<^bsub>I,A,j\<^esub>
[PROOF STEP]
apply (simp add:compos_def)
[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; j \<in> I; aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f)\<rbrakk> \<Longrightarrow> compose (carrier (a\<Pi>\<^bsub>I\<^esub> A)) (compose (carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f)) (\<pi>\<^bsub>I,A,j\<^esub>) (ainvf\<^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) = \<pi>\<^bsub>I,A,j\<^esub>
[PROOF STEP]
apply (rule funcset_eq[of _ "carrier (a\<Pi>\<^bsub>I\<^esub> A)"])
[PROOF STATE]
proof (prove)
goal (3 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; j \<in> I; aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f)\<rbrakk> \<Longrightarrow> compose (carrier (a\<Pi>\<^bsub>I\<^esub> A)) (compose (carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f)) (\<pi>\<^bsub>I,A,j\<^esub>) (ainvf\<^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> extensional (carrier (a\<Pi>\<^bsub>I\<^esub> A))
 2. \<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; j \<in> I; aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f)\<rbrakk> \<Longrightarrow> \<pi>\<^bsub>I,A,j\<^esub> \<in> extensional (carrier (a\<Pi>\<^bsub>I\<^esub> A))
 3. \<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; j \<in> I; aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f)\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier (a\<Pi>\<^bsub>I\<^esub> A). compose (carrier (a\<Pi>\<^bsub>I\<^esub> A)) (compose (carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f)) (\<pi>\<^bsub>I,A,j\<^esub>) (ainvf\<^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) x = (\<pi>\<^bsub>I,A,j\<^esub>) x
[PROOF STEP]
apply simp
[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; j \<in> I; aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f)\<rbrakk> \<Longrightarrow> \<pi>\<^bsub>I,A,j\<^esub> \<in> extensional (carrier (a\<Pi>\<^bsub>I\<^esub> A))
 2. \<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; j \<in> I; aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f)\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier (a\<Pi>\<^bsub>I\<^esub> A). compose (carrier (a\<Pi>\<^bsub>I\<^esub> A)) (compose (carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f)) (\<pi>\<^bsub>I,A,j\<^esub>) (ainvf\<^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) x = (\<pi>\<^bsub>I,A,j\<^esub>) x
[PROOF STEP]
apply (simp add:PRoject_def  prodag_carrier extensional_def)
[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; j \<in> I; aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f)\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier (a\<Pi>\<^bsub>I\<^esub> A). compose (carrier (a\<Pi>\<^bsub>I\<^esub> A)) (compose (carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f)) (\<pi>\<^bsub>I,A,j\<^esub>) (ainvf\<^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) x = (\<pi>\<^bsub>I,A,j\<^esub>) x
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 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; j \<in> I; aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); x \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A)\<rbrakk> \<Longrightarrow> compose (carrier (a\<Pi>\<^bsub>I\<^esub> A)) (compose (carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f)) (\<pi>\<^bsub>I,A,j\<^esub>) (ainvf\<^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) x = (\<pi>\<^bsub>I,A,j\<^esub>) x
[PROOF STEP]
apply (simp add:compose_def invfun_l)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 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; j \<in> I; aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); x \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A)\<rbrakk> \<Longrightarrow> (Agii (a\<Pi>\<^bsub>I\<^esub> A) f x \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<longrightarrow> (\<pi>\<^bsub>I,A,j\<^esub>) ((ainvf\<^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 x)) = (\<pi>\<^bsub>I,A,j\<^esub>) x) \<and> (Agii (a\<Pi>\<^bsub>I\<^esub> A) f x \<notin> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) \<longrightarrow> undefined = (\<pi>\<^bsub>I,A,j\<^esub>) x)
[PROOF STEP]
apply (simp add:aGroup.Agii_mem)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 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; j \<in> I; aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); x \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A)\<rbrakk> \<Longrightarrow> (\<pi>\<^bsub>I,A,j\<^esub>) ((ainvf\<^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 x)) = (\<pi>\<^bsub>I,A,j\<^esub>) x
[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. \<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; j \<in> I; aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); x \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); 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> (\<pi>\<^bsub>I,A,j\<^esub>) ((ainvf\<^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 x)) = (\<pi>\<^bsub>I,A,j\<^esub>) x
[PROOF STEP]
apply (frule_tac x = x in ainvf_l[of "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 (1 subgoal):
 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; j \<in> I; aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); x \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); 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; (ainvf\<^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 x) = x\<rbrakk> \<Longrightarrow> (\<pi>\<^bsub>I,A,j\<^esub>) ((ainvf\<^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 x)) = (\<pi>\<^bsub>I,A,j\<^esub>) x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ProjInd_aHom:"\<lbrakk>\<forall>j\<in> I. aGroup (A j); j \<in> I; f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B;
      bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) (B::'d set); j \<in> I\<rbrakk> \<Longrightarrow>
        (ProjInd I A f j) \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (A j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); j \<in> I; f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; j \<in> I\<rbrakk> \<Longrightarrow> ProjInd I A f j \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (A 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); j \<in> I; f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; j \<in> I; aGroup (a\<Pi>\<^bsub>I\<^esub> A)\<rbrakk> \<Longrightarrow> ProjInd I A f j \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (A 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); j \<in> I; f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; j \<in> I; aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f)\<rbrakk> \<Longrightarrow> ProjInd I A f j \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (A j)
[PROOF STEP]
apply (frule_tac x = j in bspec, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); j \<in> I; f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; j \<in> I; aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); aGroup (A j)\<rbrakk> \<Longrightarrow> ProjInd I A f j \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (A j)
[PROOF STEP]
apply (frule aGroup.Ag_ind_aHom[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); j \<in> I; f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; j \<in> I; aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); aGroup (A j); 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> ProjInd I A f j \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (A j)
[PROOF STEP]
apply (simp add:ProjInd_def)
[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; j \<in> I; aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (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> compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (\<pi>\<^bsub>I,A,j\<^esub>) (ainvf\<^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) \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (A 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; j \<in> I; aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (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); 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> compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (\<pi>\<^bsub>I,A,j\<^esub>) (ainvf\<^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) \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (A j)
[PROOF STEP]
apply (frule ainvf_aHom[of "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 (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; j \<in> I; aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (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); 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; ainvf\<^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 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (a\<Pi>\<^bsub>I\<^esub> A)\<rbrakk> \<Longrightarrow> compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (\<pi>\<^bsub>I,A,j\<^esub>) (ainvf\<^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) \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (A j)
[PROOF STEP]
apply (frule project_aHom[of "I" "A" "j"], 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; j \<in> I; aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (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); 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; ainvf\<^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 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (a\<Pi>\<^bsub>I\<^esub> A); \<pi>\<^bsub>I,A,j\<^esub> \<in> aHom (a\<Pi>\<^bsub>I\<^esub> A) (A j)\<rbrakk> \<Longrightarrow> compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (\<pi>\<^bsub>I,A,j\<^esub>) (ainvf\<^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) \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (A j)
[PROOF STEP]
apply (simp add:aHom_compos)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ProjInd_aHom1:"\<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)\<rbrakk> \<Longrightarrow>
        \<forall>j\<in>I. (ProjInd I A f j) \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (A 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\<rbrakk> \<Longrightarrow> \<forall>j\<in>I. ProjInd I A f j \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (A j)
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>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; j \<in> I\<rbrakk> \<Longrightarrow> ProjInd I A f j \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (A j)
[PROOF STEP]
apply (simp add:ProjInd_aHom)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ProjInd_mem_eq:"\<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; x \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f);
      y \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f);
      \<forall>j\<in>I. (ProjInd I A f j x = ProjInd I A f j y)\<rbrakk> \<Longrightarrow> x = y"
[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; x \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); y \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. ProjInd I A f j x = ProjInd I A f j y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
apply (simp add:ProjInd_def)
[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; x \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); y \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (\<pi>\<^bsub>I,A,j\<^esub>) (ainvf\<^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) x = compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (\<pi>\<^bsub>I,A,j\<^esub>) (ainvf\<^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) y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
apply (simp add:compos_def compose_def)
[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; x \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); y \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. (\<pi>\<^bsub>I,A,j\<^esub>) ((ainvf\<^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) x) = (\<pi>\<^bsub>I,A,j\<^esub>) ((ainvf\<^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) y)\<rbrakk> \<Longrightarrow> x = y
[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; x \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); y \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. (\<pi>\<^bsub>I,A,j\<^esub>) ((ainvf\<^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) x) = (\<pi>\<^bsub>I,A,j\<^esub>) ((ainvf\<^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) y); aGroup (a\<Pi>\<^bsub>I\<^esub> A)\<rbrakk> \<Longrightarrow> x = y
[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; x \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); y \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. (\<pi>\<^bsub>I,A,j\<^esub>) ((ainvf\<^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) x) = (\<pi>\<^bsub>I,A,j\<^esub>) ((ainvf\<^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) y); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f)\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
apply (frule aGroup.Ag_ind_aHom[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; x \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); y \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. (\<pi>\<^bsub>I,A,j\<^esub>) ((ainvf\<^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) x) = (\<pi>\<^bsub>I,A,j\<^esub>) ((ainvf\<^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) y); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (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> x = y
[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; x \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); y \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. (\<pi>\<^bsub>I,A,j\<^esub>) ((ainvf\<^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) x) = (\<pi>\<^bsub>I,A,j\<^esub>) ((ainvf\<^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) y); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (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); 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> x = y
[PROOF STEP]
apply (frule ainvf_aHom[of "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 (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; x \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); y \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. (\<pi>\<^bsub>I,A,j\<^esub>) ((ainvf\<^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) x) = (\<pi>\<^bsub>I,A,j\<^esub>) ((ainvf\<^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) y); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (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); 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; ainvf\<^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 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (a\<Pi>\<^bsub>I\<^esub> A)\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
apply (frule aHom_mem[of "Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f" "a\<Pi>\<^bsub>I\<^esub> A" "ainvf\<^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" "x"], assumption+,
       frule aHom_mem[of "Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f" "a\<Pi>\<^bsub>I\<^esub> A" "ainvf\<^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" "y"], 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; x \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); y \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. (\<pi>\<^bsub>I,A,j\<^esub>) ((ainvf\<^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) x) = (\<pi>\<^bsub>I,A,j\<^esub>) ((ainvf\<^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) y); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (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); 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; ainvf\<^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 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (a\<Pi>\<^bsub>I\<^esub> A); (ainvf\<^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) x \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); (ainvf\<^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) y \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A)\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
apply (frule direct_prod_mem_eq[of "I" "A" "(ainvf\<^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) x" "(ainvf\<^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) y"], 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; x \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); y \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. (\<pi>\<^bsub>I,A,j\<^esub>) ((ainvf\<^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) x) = (\<pi>\<^bsub>I,A,j\<^esub>) ((ainvf\<^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) y); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (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); 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; ainvf\<^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 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (a\<Pi>\<^bsub>I\<^esub> A); (ainvf\<^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) x \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); (ainvf\<^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) y \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); (ainvf\<^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) x = (ainvf\<^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) y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
apply (thin_tac "ainvf\<^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
     \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (a\<Pi>\<^bsub>I\<^esub> 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; x \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); y \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. (\<pi>\<^bsub>I,A,j\<^esub>) ((ainvf\<^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) x) = (\<pi>\<^bsub>I,A,j\<^esub>) ((ainvf\<^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) y); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (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); 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; (ainvf\<^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) x \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); (ainvf\<^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) y \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); (ainvf\<^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) x = (ainvf\<^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) y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
apply (frule ainvf_bijec[of "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 (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; x \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); y \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. (\<pi>\<^bsub>I,A,j\<^esub>) ((ainvf\<^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) x) = (\<pi>\<^bsub>I,A,j\<^esub>) ((ainvf\<^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) y); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (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); 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; (ainvf\<^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) x \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); (ainvf\<^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) y \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); (ainvf\<^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) x = (ainvf\<^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) y; bijec\<^bsub>Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f,(a\<Pi>\<^bsub>I\<^esub> A)\<^esub> (ainvf\<^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> x = y
[PROOF STEP]
apply (thin_tac "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")
[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; x \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); y \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. (\<pi>\<^bsub>I,A,j\<^esub>) ((ainvf\<^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) x) = (\<pi>\<^bsub>I,A,j\<^esub>) ((ainvf\<^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) y); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (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); (ainvf\<^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) x \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); (ainvf\<^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) y \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); (ainvf\<^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) x = (ainvf\<^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) y; bijec\<^bsub>Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f,(a\<Pi>\<^bsub>I\<^esub> A)\<^esub> (ainvf\<^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> x = y
[PROOF STEP]
apply (unfold bijec_def, frule conjunct1, fold bijec_def)
[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; x \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); y \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. (\<pi>\<^bsub>I,A,j\<^esub>) ((ainvf\<^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) x) = (\<pi>\<^bsub>I,A,j\<^esub>) ((ainvf\<^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) y); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (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); (ainvf\<^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) x \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); (ainvf\<^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) y \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); (ainvf\<^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) x = (ainvf\<^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) y; bijec\<^bsub>Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f,(a\<Pi>\<^bsub>I\<^esub> A)\<^esub> (ainvf\<^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); injec\<^bsub>Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f,(a\<Pi>\<^bsub>I\<^esub> A)\<^esub> (ainvf\<^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> x = y
[PROOF STEP]
apply (frule injec_inj_on[of "Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f" "a\<Pi>\<^bsub>I\<^esub> A" "ainvf\<^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"], 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; x \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); y \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. (\<pi>\<^bsub>I,A,j\<^esub>) ((ainvf\<^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) x) = (\<pi>\<^bsub>I,A,j\<^esub>) ((ainvf\<^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) y); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (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); (ainvf\<^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) x \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); (ainvf\<^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) y \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); (ainvf\<^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) x = (ainvf\<^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) y; bijec\<^bsub>Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f,(a\<Pi>\<^bsub>I\<^esub> A)\<^esub> (ainvf\<^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); injec\<^bsub>Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f,(a\<Pi>\<^bsub>I\<^esub> A)\<^esub> (ainvf\<^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); inj_on (ainvf\<^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) (carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f))\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
apply (simp add:injective_iff[THEN sym, of "ainvf\<^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" "carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f)" "x" "y"])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ProjInd_mem_eq1:"\<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;
      h \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f);
      \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (ProjInd I A f j) h = ProjInd I A f j\<rbrakk>       \<Longrightarrow> h = ag_idmap (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f)"
[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; h \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (ProjInd I A f j) h = ProjInd I A f j\<rbrakk> \<Longrightarrow> h = aI\<^bsub>Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub>
[PROOF STEP]
apply (rule funcset_eq[of _ "carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f)"])
[PROOF STATE]
proof (prove)
goal (3 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; h \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (ProjInd I A f j) h = ProjInd I A f j\<rbrakk> \<Longrightarrow> h \<in> extensional (carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f))
 2. \<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; h \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (ProjInd I A f j) h = ProjInd I A f j\<rbrakk> \<Longrightarrow> aI\<^bsub>Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> \<in> extensional (carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f))
 3. \<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; h \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (ProjInd I A f j) h = ProjInd I A f j\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f). h x = aI\<^bsub>Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> x
[PROOF STEP]
apply (simp add:aHom_def)
[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; h \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (ProjInd I A f j) h = ProjInd I A f j\<rbrakk> \<Longrightarrow> aI\<^bsub>Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> \<in> extensional (carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f))
 2. \<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; h \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (ProjInd I A f j) h = ProjInd I A f j\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f). h x = aI\<^bsub>Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> x
[PROOF STEP]
apply (simp add:ag_idmap_def)
[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; h \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (ProjInd I A f j) h = ProjInd I A f j\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f). h x = aI\<^bsub>Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> x
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 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; h \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (ProjInd I A f j) h = ProjInd I A f j; x \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f)\<rbrakk> \<Longrightarrow> h x = aI\<^bsub>Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f\<^esub> x
[PROOF STEP]
apply (simp add:ag_idmap_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 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; h \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (ProjInd I A f j) h = ProjInd I A f j; x \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f)\<rbrakk> \<Longrightarrow> h x = x
[PROOF STEP]
apply (frule prodag_aGroup[of "I" "A"],
        frule aGroup.Ag_ind_aGroup[of "a\<Pi>\<^bsub>I\<^esub> A" "f" "B"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 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; h \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (ProjInd I A f j) h = ProjInd I A f j; x \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f)\<rbrakk> \<Longrightarrow> h x = x
[PROOF STEP]
apply (frule_tac a = x in aHom_mem[of "Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f" "Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f"
        "h"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 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; h \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (ProjInd I A f j) h = ProjInd I A f j; x \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); h x \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f)\<rbrakk> \<Longrightarrow> h x = x
[PROOF STEP]
apply (rule_tac x = "h x" and y = x in ProjInd_mem_eq[of "I" "A" "f" "B" "S"],
        assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 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; h \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (ProjInd I A f j) h = ProjInd I A f j; x \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); h 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 x
[PROOF STEP]
apply (rotate_tac 1,
        rule ballI,
        frule_tac x = j in bspec, assumption,
        thin_tac "\<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (ProjInd I A f j) h =
               ProjInd I A f j")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x j. \<lbrakk>f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; h \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); x \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); h x \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. aGroup (A j); j \<in> I; compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (ProjInd I A f j) h = ProjInd I A f j\<rbrakk> \<Longrightarrow> ProjInd I A f j (h x) = ProjInd I A f j x
[PROOF STEP]
apply (simp add:compos_def compose_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x j. \<lbrakk>f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; h \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); x \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); h x \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. aGroup (A j); j \<in> I; (\<lambda>x\<in>carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f). ProjInd I A f j (h x)) = ProjInd I A f j\<rbrakk> \<Longrightarrow> ProjInd I A f j (h x) = ProjInd I A f j x
[PROOF STEP]
apply (subgoal_tac "(\<lambda>x\<in>carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f). ProjInd I A f j (h x)) x
                    = ProjInd I A f j x",
        thin_tac "(\<lambda>x\<in>carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f). ProjInd I A f j (h x)) =
           ProjInd I A f j")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x j. \<lbrakk>f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; h \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); x \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); h x \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. aGroup (A j); j \<in> I; (\<lambda>x\<in>carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f). ProjInd I A f j (h x)) x = ProjInd I A f j x\<rbrakk> \<Longrightarrow> ProjInd I A f j (h x) = ProjInd I A f j x
 2. \<And>x j. \<lbrakk>f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to f (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup S; h \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); x \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); h x \<in> carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f); \<forall>j\<in>I. aGroup (A j); j \<in> I; (\<lambda>x\<in>carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f). ProjInd I A f j (h x)) = ProjInd I A f j\<rbrakk> \<Longrightarrow> (\<lambda>x\<in>carrier (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f). ProjInd I A f j (h x)) x = ProjInd I A f j x
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Ag_ind_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); j \<in> I\<rbrakk> \<Longrightarrow>
      compos (a\<Pi>\<^bsub>I\<^esub> A) (ProjInd I A f j) (Agii (a\<Pi>\<^bsub>I\<^esub> A) f) =  PRoject I A 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; j \<in> I\<rbrakk> \<Longrightarrow> compos (a\<Pi>\<^bsub>I\<^esub> A) (ProjInd I A f j) (Agii (a\<Pi>\<^bsub>I\<^esub> A) f) = \<pi>\<^bsub>I,A,j\<^esub>
[PROOF STEP]
apply (simp add:ProjInd_def)
[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; j \<in> I\<rbrakk> \<Longrightarrow> compos (a\<Pi>\<^bsub>I\<^esub> A) (compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) f) (\<pi>\<^bsub>I,A,j\<^esub>) (ainvf\<^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) = \<pi>\<^bsub>I,A,j\<^esub>
[PROOF STEP]
apply (simp add:Ag_ind_triangle)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done