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 5 :: thesis: for b_{1}, b_{2}, b_{3} being set holds

( not b_{1} in (the_hom_sets_of C) . (i,j) or not b_{2} in (the_hom_sets_of C) . (j,k) or not b_{3} in (the_hom_sets_of C) . (k,l) or ((the_comps_of C) . (i,k,l)) . (b_{3},(((the_comps_of C) . (i,j,k)) . (b_{2},b_{1}))) = ((the_comps_of C) . (i,j,l)) . ((((the_comps_of C) . (j,k,l)) . (b_{3},b_{2})),b_{1}) )

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 5;

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 5;

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 5;

A4: ( Hom (j,l) <> {} & ((the_comps_of C) . (j,k,l)) . (h,g) = h9 * g9 ) by A2, A3, Th13, CAT_1:24;

( Hom (i,k) <> {} & ((the_comps_of C) . (i,j,k)) . (g,f) = g9 * f9 ) by A1, A2, Th13, CAT_1:24;

hence ((the_comps_of C) . (i,k,l)) . (h,(((the_comps_of C) . (i,j,k)) . (g,f))) = h9 * (g9 * f9) by A3, Th13

.= (h9 * g9) * f9 by A1, A2, A3, CAT_1:25

.= ((the_comps_of C) . (i,j,l)) . ((((the_comps_of C) . (j,k,l)) . (h,g)),f) by A1, A4, Th13 ;

:: thesis: verum

let i, j, k, l be Object of C; :: according to ALTCAT_1:def 5 :: thesis: for b

( not 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 5;

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 5;

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 5;

A4: ( Hom (j,l) <> {} & ((the_comps_of C) . (j,k,l)) . (h,g) = h9 * g9 ) by A2, A3, Th13, CAT_1:24;

( Hom (i,k) <> {} & ((the_comps_of C) . (i,j,k)) . (g,f) = g9 * f9 ) by A1, A2, Th13, CAT_1:24;

hence ((the_comps_of C) . (i,k,l)) . (h,(((the_comps_of C) . (i,j,k)) . (g,f))) = h9 * (g9 * f9) by A3, Th13

.= (h9 * g9) * f9 by A1, A2, A3, CAT_1:25

.= ((the_comps_of C) . (i,j,l)) . ((((the_comps_of C) . (j,k,l)) . (h,g)),f) by A1, A4, Th13 ;

:: thesis: verum