let C be Category; 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; the Comp of C .: [:(Hom (j,k)),(Hom (i,j)):] c= Hom (i,k)
let e be object ; TARSKI:def 3 ( 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)):]
; e in Hom (i,k)
then consider x being object 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 6;
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:21;
A5:
x `2 in Hom (i,j)
by A2, MCART_1:10;
then A6:
z is Morphism of i,j
by CAT_1:def 5;
A7:
x `1 in Hom (j,k)
by A2, MCART_1:10;
then
y is Morphism of j,k
by CAT_1:def 5;
then
y (*) z in Hom (i,k)
by A7, A5, A6, CAT_1:23;
hence
e in Hom (i,k)
by A1, A4, CAT_1:def 1; verum