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

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