let A be Category; 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)); ( Obj F is one-to-one & F is faithful implies F is one-to-one )
assume A1:
Obj F is one-to-one
; ( not F is faithful or F is one-to-one )
assume A2:
F is faithful
; 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
let x1,
x2 be
object ;
( 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
;
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;
verum
end;
hence
F is one-to-one
by FUNCT_1:def 4; verum