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

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