let A be Category; :: thesis: for F being Contravariant_Functor of A, Functors (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,()); :: 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
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 ;
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
.= (Obj F) . (dom m2) by OPPCAT_1:32 ;
then A5: ( m2 is Morphism of dom m2, cod m2 & dom m1 = dom m2 ) by ;
A6: ( m1 is Morphism of dom m1, cod m1 & Hom ((dom m1),(cod m1)) <> {} ) by ;
(Obj F) . (cod m1) = dom (F . m29) by
.= (Obj F) . (cod m2) by OPPCAT_1:32 ;
then m2 is Morphism of dom m1, cod m1 by ;
hence x1 = x2 by A2, A4, A6; :: thesis: verum
end;
hence F is one-to-one by FUNCT_1:def 4; :: thesis: verum