let C be Category; :: thesis: the_comps_of C is associative
let i, j, k, l be Object of C; :: according to ALTCAT_1:def 7 :: thesis: for b₁, b₂, b₃ being set holds
( not b₁ in (the_hom_sets_of C) . i,j or not b₂ in (the_hom_sets_of C) . j,k or not b₃ in (the_hom_sets_of C) . k,l or ((the_comps_of C) . i,k,l) . b₃,(((the_comps_of C) . i,j,k) . b₂,b₁) = ((the_comps_of C) . i,j,l) . (((the_comps_of C) . j,k,l) . b₃,b₂),b₁ )
let f, g, h be set ; :: thesis: ( not f in (the_hom_sets_of C) . i,j or not g in (the_hom_sets_of C) . j,k or not h in (the_hom_sets_of C) . k,l or ((the_comps_of C) . i,k,l) . h,(((the_comps_of C) . i,j,k) . g,f) = ((the_comps_of C) . i,j,l) . (((the_comps_of C) . j,k,l) . h,g),f )
assume f in (the_hom_sets_of C) . i,j ; :: thesis: ( not g in (the_hom_sets_of C) . j,k or not h in (the_hom_sets_of C) . k,l or ((the_comps_of C) . i,k,l) . h,(((the_comps_of C) . i,j,k) . g,f) = ((the_comps_of C) . i,j,l) . (((the_comps_of C) . j,k,l) . h,g),f )
then A1: f in Hom i,j by Def3;
then reconsider f9 = f as Morphism of i,j by CAT_1:def 7;
assume g in (the_hom_sets_of C) . j,k ; :: thesis: ( not h in (the_hom_sets_of C) . k,l or ((the_comps_of C) . i,k,l) . h,(((the_comps_of C) . i,j,k) . g,f) = ((the_comps_of C) . i,j,l) . (((the_comps_of C) . j,k,l) . h,g),f )
then A2: g in Hom j,k by Def3;
then reconsider g9 = g as Morphism of j,k by CAT_1:def 7;
assume h in (the_hom_sets_of C) . k,l ; :: thesis: ((the_comps_of C) . i,k,l) . h,(((the_comps_of C) . i,j,k) . g,f) = ((the_comps_of C) . i,j,l) . (((the_comps_of C) . j,k,l) . h,g),f
then A3: h in Hom k,l by Def3;
then reconsider h9 = h as Morphism of k,l by CAT_1:def 7;
A4: ( Hom j,l <> {} & ((the_comps_of C) . j,k,l) . h,g = h9 * g9 ) by A2, A3, Th14, CAT_1:52;
( Hom i,k <> {} & ((the_comps_of C) . i,j,k) . g,f = g9 * f9 ) by A1, A2, Th14, CAT_1:52;
hence ((the_comps_of C) . i,k,l) . h,(((the_comps_of C) . i,j,k) . g,f) = h9 * (g9 * f9) by A3, Th14
.= (h9 * g9) * f9 by A1, A2, A3, CAT_1:54
.= ((the_comps_of C) . i,j,l) . (((the_comps_of C) . j,k,l) . h,g),f by A1, A4, Th14 ;
:: thesis: verum