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 f' = 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 g' = 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 h' = h as Morphism of k,l by CAT_1:def 7;
A4: Hom i,k <> {} by A1, A2, CAT_1:52;
A5: Hom j,l <> {} by A2, A3, CAT_1:52;
A6: ((the_comps_of C) . i,j,k) . g,f = g' * f' by A1, A2, Th14;
A7: ((the_comps_of C) . j,k,l) . h,g = h' * g' by A2, A3, Th14;
thus ((the_comps_of C) . i,k,l) . h,(((the_comps_of C) . i,j,k) . g,f) = h' * (g' * f') by A3, A4, A6, Th14
.= (h' * g') * f' 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, A5, A7, Th14 ; :: thesis: verum