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: g in Hom j,k by A2, CAT_1:def 7;
then A4: g in (the_hom_sets_of C) . j,k by Def3;
A5: f in Hom i,j by A1, CAT_1:def 7;
then f in (the_hom_sets_of C) . i,j by Def3;
then A6: [g,f] in [:((the_hom_sets_of C) . j,k),((the_hom_sets_of C) . i,j):] by A4, ZFMISC_1:106;
A7: dom g = j by A3, CAT_1:18
.= cod f by A5, CAT_1:18 ;
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 A6, FUNCT_1:72
.= g * f by A7, CAT_1:41
.= g * f by A1, A2, CAT_1:def 13 ; :: thesis: verum