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 object ; :: 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:21;
e `1 in Hom (j,k) by A1, MCART_1:10;
then dom y = j by CAT_1:1
.= cod x by A2, CAT_1:1 ;
hence e in dom the Comp of C by A3, CAT_1:15; :: thesis: verum