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

assume A3: Hom (T . c),(T . c') <> {} ; :: thesis: hom T,c,c' is one-to-one

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 ( f1 in Hom c,c' & f2 in Hom c,c' ) ; :: thesis: ( (hom T,c,c') . f1 = (hom T,c,c') . f2 implies f1 = f2 )
then A4: ( f1 is Morphism of c,c' & f2 is Morphism of c,c' & Hom c,c' <> {} ) by Def7;
then ( T . f1 = (hom T,c,c') . f1 & T . f2 = (hom T,c,c') . f2 ) by Th131;
hence ( (hom T,c,c') . f1 = (hom T,c,c') . f2 implies f1 = f2 ) by A1, A4, Def24; :: thesis: verum

end;

hence hom T,c,c' is one-to-one by A3, FUNCT_2:25; :: thesis: verum

end;

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

end;

assume A5: 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 A6: 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 )
( Hom (T . c),(T . c') <> {} & f1 in Hom c,c' & f2 in Hom c,c' & hom T,c,c' is one-to-one & T . f1 = (hom T,c,c') . f1 & T . f2 = (hom T,c,c') . f2 ) by A5, A6, Def7, Th126, Th131;
hence ( T . f1 = T . f2 implies f1 = f2 ) by FUNCT_2:25; :: thesis: verum