let C, D be Category; :: thesis: for T being Functor of C,D holds
( T is faithful iff for c, c' being Object of C holds hom T,c,c' is one-to-one )
let T be Functor of C,D; :: thesis: ( T is faithful iff for c, c' being Object of C holds hom T,c,c' is one-to-one )
thus ( T is faithful implies for c, c' being Object of C holds hom T,c,c' is one-to-one ) :: thesis: ( ( for c, c' being Object of C holds hom T,c,c' is one-to-one ) implies T is faithful )

proof

assume A1: T is faithful ; :: thesis: for c, c' being Object of C holds hom T,c,c' is one-to-one
let c, c' be Object of C; :: thesis: hom T,c,c' is one-to-one

now

A2: now

let f1, f2 be set ; :: thesis: ( f1 in Hom c,c' & f2 in Hom c,c' & (hom T,c,c') . f1 = (hom T,c,c') . f2 implies f1 = f2 )
assume that
A3: f1 in Hom c,c' and
A4: f2 in Hom c,c' ; :: thesis: ( (hom T,c,c') . f1 = (hom T,c,c') . f2 implies f1 = f2 )
A5: f2 is Morphism of c,c' by A4, Def7;
then A6: T . f2 = (hom T,c,c') . f2 by A3, Th131;
A7: f1 is Morphism of c,c' by A3, Def7;
then T . f1 = (hom T,c,c') . f1 by A3, Th131;
hence ( (hom T,c,c') . f1 = (hom T,c,c') . f2 implies f1 = f2 ) by A1, A3, A7, A5, A6, Def24; :: thesis: verum

end;

assume Hom (T . c),(T . c') <> {} ; :: thesis: hom T,c,c' is one-to-one
hence hom T,c,c' is one-to-one by A2, FUNCT_2:25; :: thesis: verum

end;

hence hom T,c,c' is one-to-one ; :: thesis: verum

end;

assume A8: for c, c' being Object of C holds hom T,c,c' is one-to-one ; :: thesis: T is faithful
let c, c' be Object of C; :: according to CAT_1:def 24 :: thesis: ( Hom c,c' <> {} implies for f1, f2 being Morphism of c,c' st T . f1 = T . f2 holds
f1 = f2 )
assume A9: Hom c,c' <> {} ; :: thesis: for f1, f2 being Morphism of c,c' st T . f1 = T . f2 holds
f1 = f2
let f1, f2 be Morphism of c,c'; :: thesis: ( T . f1 = T . f2 implies f1 = f2 )
A10: T . f2 = (hom T,c,c') . f2 by A9, Th131;
A11: ( f2 in Hom c,c' & T . f1 = (hom T,c,c') . f1 ) by A9, Def7, Th131;
A12: hom T,c,c' is one-to-one by A8;
( Hom (T . c),(T . c') <> {} & f1 in Hom c,c' ) by A9, Def7, Th126;
hence ( T . f1 = T . f2 implies f1 = f2 ) by A12, A11, A10, FUNCT_2:25; :: thesis: verum