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 set ; :: 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 set 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 12;
A4: ( x `1 in Hom j,k & x `2 in Hom i,j ) by A2, MCART_1:10;
reconsider y = x `1 , z = x `2 as Morphism of C by A2, MCART_1:10;
A5: x = [y,z] by A2, MCART_1:23;
A6: e = the Comp of C . y,z by A2, A3, MCART_1:23;
( y is Morphism of j,k & z is Morphism of i,j ) by A4, CAT_1:def 7;
then y * z in Hom i,k by A4, CAT_1:51;
hence e in Hom i,k by A1, A5, A6, CAT_1:def 4; :: thesis: verum