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