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