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 5;
then A4: g in (the_hom_sets_of C) . (j,k) by Def3;
A5: f in Hom (i,j) by A1, CAT_1:def 5;
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:87;
A7: dom g = j by A3, CAT_1:1
.= cod f by A5, CAT_1:1 ;
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:49
.= g (*) f by A7, CAT_1:16
.= g * f by A1, A2, CAT_1:def 13 ; :: thesis: verum