let C be Category; :: thesis: for i, j, k being Object of C holds [:(Hom j,k),(Hom i,j):] c= dom the Comp of C
let i, j, k be Object of C; :: thesis: [:(Hom j,k),(Hom i,j):] c= dom the Comp of C
let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in [:(Hom j,k),(Hom i,j):] or e in dom the Comp of C )
assume A1: e in [:(Hom j,k),(Hom i,j):] ; :: thesis: e in dom the Comp of C
then reconsider y = e `1 , x = e `2 as Morphism of C by MCART_1:10;
A2: e `2 in Hom i,j by A1, MCART_1:10;
A3: e = [y,x] by A1, MCART_1:23;
e `1 in Hom j,k by A1, MCART_1:10;
then dom y = j by CAT_1:18
.= cod x by A2, CAT_1:18 ;
hence e in dom the Comp of C by A3, CAT_1:40; :: thesis: verum