let A be Category; :: thesis: for F being Contravariant_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 Contravariant_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 Contravariant_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 m29 = m2 as Morphism of dom m2, cod m2 by CAT_1:4;

(Obj F) . (dom m1) = cod (F . m29) by A4, OPPCAT_1:32

.= (Obj F) . (dom m2) by OPPCAT_1:32 ;

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

A6: ( m1 is Morphism of dom m1, cod m1 & Hom ((dom m1),(cod m1)) <> {} ) by CAT_1:2, CAT_1:4;

(Obj F) . (cod m1) = dom (F . m29) by A4, OPPCAT_1:32

.= (Obj F) . (cod m2) by OPPCAT_1:32 ;

then m2 is Morphism of dom m1, cod m1 by A1, A5, FUNCT_2:19;

hence x1 = x2 by A2, A4, A6; :: 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 m29 = m2 as Morphism of dom m2, cod m2 by CAT_1:4;

(Obj F) . (dom m1) = cod (F . m29) by A4, OPPCAT_1:32

.= (Obj F) . (dom m2) by OPPCAT_1:32 ;

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

A6: ( m1 is Morphism of dom m1, cod m1 & Hom ((dom m1),(cod m1)) <> {} ) by CAT_1:2, CAT_1:4;

(Obj F) . (cod m1) = dom (F . m29) by A4, OPPCAT_1:32

.= (Obj F) . (cod m2) by OPPCAT_1:32 ;

then m2 is Morphism of dom m1, cod m1 by A1, A5, FUNCT_2:19;

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