let C be Category; the_comps_of C is associative
let i, j, k, l be Object of C; ALTCAT_1:def 5 for b1, b2, b3 being set holds
( not b1 in (the_hom_sets_of C) . (i,j) or not b2 in (the_hom_sets_of C) . (j,k) or not b3 in (the_hom_sets_of C) . (k,l) or ((the_comps_of C) . (i,k,l)) . (b3,(((the_comps_of C) . (i,j,k)) . (b2,b1))) = ((the_comps_of C) . (i,j,l)) . ((((the_comps_of C) . (j,k,l)) . (b3,b2)),b1) )
let f, g, h be set ; ( 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)
; ( 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)
; ( 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)
; ((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
;
verum