let C be Category; :: thesis: for i, j, k being Object of C holds the Comp of C .: [:(Hom (j,k)),(Hom (i,j)):] c= Hom (i,k)

let i, j, k be Object of C; :: thesis: the Comp of C .: [:(Hom (j,k)),(Hom (i,j)):] c= Hom (i,k)

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in the Comp of C .: [:(Hom (j,k)),(Hom (i,j)):] or e in Hom (i,k) )

assume e in the Comp of C .: [:(Hom (j,k)),(Hom (i,j)):] ; :: thesis: e in Hom (i,k)

then consider x being object such that

A1: x in dom the Comp of C and

A2: x in [:(Hom (j,k)),(Hom (i,j)):] and

A3: e = the Comp of C . x by FUNCT_1:def 6;

reconsider y = x `1 , z = x `2 as Morphism of C by A2, MCART_1:10;

A4: ( x = [y,z] & e = the Comp of C . (y,z) ) by A2, A3, MCART_1:21;

A5: x `2 in Hom (i,j) by A2, MCART_1:10;

then A6: z is Morphism of i,j by CAT_1:def 5;

A7: x `1 in Hom (j,k) by A2, MCART_1:10;

then y is Morphism of j,k by CAT_1:def 5;

then y (*) z in Hom (i,k) by A7, A5, A6, CAT_1:23;

hence e in Hom (i,k) by A1, A4, CAT_1:def 1; :: thesis: verum

let i, j, k be Object of C; :: thesis: the Comp of C .: [:(Hom (j,k)),(Hom (i,j)):] c= Hom (i,k)

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in the Comp of C .: [:(Hom (j,k)),(Hom (i,j)):] or e in Hom (i,k) )

assume e in the Comp of C .: [:(Hom (j,k)),(Hom (i,j)):] ; :: thesis: e in Hom (i,k)

then consider x being object such that

A1: x in dom the Comp of C and

A2: x in [:(Hom (j,k)),(Hom (i,j)):] and

A3: e = the Comp of C . x by FUNCT_1:def 6;

reconsider y = x `1 , z = x `2 as Morphism of C by A2, MCART_1:10;

A4: ( x = [y,z] & e = the Comp of C . (y,z) ) by A2, A3, MCART_1:21;

A5: x `2 in Hom (i,j) by A2, MCART_1:10;

then A6: z is Morphism of i,j by CAT_1:def 5;

A7: x `1 in Hom (j,k) by A2, MCART_1:10;

then y is Morphism of j,k by CAT_1:def 5;

then y (*) z in Hom (i,k) by A7, A5, A6, CAT_1:23;

hence e in Hom (i,k) by A1, A4, CAT_1:def 1; :: thesis: verum