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;
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:23;
A5: x `2 in Hom i,j by A2, MCART_1:10;
then A6: z is Morphism of i,j by CAT_1:def 7;
A7: x `1 in Hom j,k by A2, MCART_1:10;
then y is Morphism of j,k by CAT_1:def 7;
then y * z in Hom i,k by A7, A5, A6, CAT_1:51;
hence e in Hom i,k by A1, A4, CAT_1:def 4; :: thesis: verum