let C be Category; :: thesis: for i, j, k being Object of C st Hom i,j <> {} & Hom j,k <> {} holds
for f being Morphism of i,j
for g being Morphism of j,k holds ((the_comps_of C) . i,j,k) . g,f = g * f
let i, j, k be Object of C; :: thesis: ( Hom i,j <> {} & Hom j,k <> {} implies for f being Morphism of i,j
for g being Morphism of j,k holds ((the_comps_of C) . i,j,k) . g,f = g * f )
assume that
A1: Hom i,j <> {} and
A2: Hom j,k <> {} ; :: thesis: for f being Morphism of i,j
for g being Morphism of j,k holds ((the_comps_of C) . i,j,k) . g,f = g * f
let f be Morphism of i,j; :: thesis: for g being Morphism of j,k holds ((the_comps_of C) . i,j,k) . g,f = g * f
let g be Morphism of j,k; :: thesis: ((the_comps_of C) . i,j,k) . g,f = g * f
A3: f in Hom i,j by A1, CAT_1:def 7;
A4: g in Hom j,k by A2, CAT_1:def 7;
then A5: dom g = j by CAT_1:18
.= cod f by A3, CAT_1:18 ;
A6: f in (the_hom_sets_of C) . i,j by A3, Def3;
g in (the_hom_sets_of C) . j,k by A4, Def3;
then A7: [g,f] in [:((the_hom_sets_of C) . j,k),((the_hom_sets_of C) . i,j):] by A6, ZFMISC_1:106;
thus ((the_comps_of C) . i,j,k) . g,f = (the Comp of C | [:((the_hom_sets_of C) . j,k),((the_hom_sets_of C) . i,j):]) . [g,f] by Def4
.= the Comp of C . g,f by A7, FUNCT_1:72
.= g * f by A5, CAT_1:41
.= g * f by A1, A2, CAT_1:def 13 ; :: thesis: verum