let A be Category; :: thesis: for F being Functor of A, Functors (A,(EnsHom A)) st Obj F is one-to-one & F is faithful holds

F is one-to-one

let F be Functor of A, Functors (A,(EnsHom A)); :: thesis: ( Obj F is one-to-one & F is faithful implies F is one-to-one )

assume A1: Obj F is one-to-one ; :: thesis: ( not F is faithful or F is one-to-one )

assume A2: F is faithful ; :: thesis: F is one-to-one

for x1, x2 being object st x1 in dom F & x2 in dom F & F . x1 = F . x2 holds

x1 = x2

F is one-to-one

let F be Functor of A, Functors (A,(EnsHom A)); :: thesis: ( Obj F is one-to-one & F is faithful implies F is one-to-one )

assume A1: Obj F is one-to-one ; :: thesis: ( not F is faithful or F is one-to-one )

assume A2: F is faithful ; :: thesis: F is one-to-one

for x1, x2 being object st x1 in dom F & x2 in dom F & F . x1 = F . x2 holds

x1 = x2

proof

hence
F is one-to-one
by FUNCT_1:def 4; :: thesis: verum
let x1, x2 be object ; :: thesis: ( x1 in dom F & x2 in dom F & F . x1 = F . x2 implies x1 = x2 )

assume that

A3: ( x1 in dom F & x2 in dom F ) and

A4: F . x1 = F . x2 ; :: thesis: x1 = x2

reconsider m1 = x1, m2 = x2 as Morphism of A by A3, FUNCT_2:def 1;

set o1 = dom m1;

set o2 = cod m1;

set o3 = dom m2;

set o4 = cod m2;

reconsider m19 = m1 as Morphism of dom m1, cod m1 by CAT_1:4;

reconsider m29 = m2 as Morphism of dom m2, cod m2 by CAT_1:4;

A5: Hom ((dom m1),(cod m1)) <> {} by CAT_1:2;

then A6: Hom ((F . (dom m1)),(F . (cod m1))) <> {} by CAT_1:84;

A7: Hom ((dom m2),(cod m2)) <> {} by CAT_1:2;

then A8: Hom ((F . (dom m2)),(F . (cod m2))) <> {} by CAT_1:84;

A9: F /. m19 = F . m2 by A4, A5, CAT_3:def 10

.= F /. m29 by A7, CAT_3:def 10 ;

(Obj F) . (dom m1) = F . (dom m1)

.= dom (F /. m29) by A9, A6, CAT_1:5

.= (Obj F) . (dom m2) by A8, CAT_1:5 ;

then A10: ( m2 is Morphism of dom m2, cod m2 & dom m1 = dom m2 ) by A1, CAT_1:4, FUNCT_2:19;

(Obj F) . (cod m1) = F . (cod m1)

.= cod (F /. m29) by A9, A6, CAT_1:5

.= (Obj F) . (cod m2) by A8, CAT_1:5 ;

then ( m1 is Morphism of dom m1, cod m1 & m2 is Morphism of dom m1, cod m1 ) by A1, A10, CAT_1:4, FUNCT_2:19;

hence x1 = x2 by A2, A4, A5; :: thesis: verum

end;assume that

A3: ( x1 in dom F & x2 in dom F ) and

A4: F . x1 = F . x2 ; :: thesis: x1 = x2

reconsider m1 = x1, m2 = x2 as Morphism of A by A3, FUNCT_2:def 1;

set o1 = dom m1;

set o2 = cod m1;

set o3 = dom m2;

set o4 = cod m2;

reconsider m19 = m1 as Morphism of dom m1, cod m1 by CAT_1:4;

reconsider m29 = m2 as Morphism of dom m2, cod m2 by CAT_1:4;

A5: Hom ((dom m1),(cod m1)) <> {} by CAT_1:2;

then A6: Hom ((F . (dom m1)),(F . (cod m1))) <> {} by CAT_1:84;

A7: Hom ((dom m2),(cod m2)) <> {} by CAT_1:2;

then A8: Hom ((F . (dom m2)),(F . (cod m2))) <> {} by CAT_1:84;

A9: F /. m19 = F . m2 by A4, A5, CAT_3:def 10

.= F /. m29 by A7, CAT_3:def 10 ;

(Obj F) . (dom m1) = F . (dom m1)

.= dom (F /. m29) by A9, A6, CAT_1:5

.= (Obj F) . (dom m2) by A8, CAT_1:5 ;

then A10: ( m2 is Morphism of dom m2, cod m2 & dom m1 = dom m2 ) by A1, CAT_1:4, FUNCT_2:19;

(Obj F) . (cod m1) = F . (cod m1)

.= cod (F /. m29) by A9, A6, CAT_1:5

.= (Obj F) . (cod m2) by A8, CAT_1:5 ;

then ( m1 is Morphism of dom m1, cod m1 & m2 is Morphism of dom m1, cod m1 ) by A1, A10, CAT_1:4, FUNCT_2:19;

hence x1 = x2 by A2, A4, A5; :: thesis: verum