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

proof

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

now :: thesis: ( Hom ((T . c),(T . c9)) <> {} implies hom (T,c,c9) is one-to-one )

A2: now :: thesis: for f1, f2 being object st f1 in Hom (c,c9) & f2 in Hom (c,c9) & (hom (T,c,c9)) . f1 = (hom (T,c,c9)) . f2 holds
f1 = f2

let f1, f2 be object ; :: thesis: ( f1 in Hom (c,c9) & f2 in Hom (c,c9) & (hom (T,c,c9)) . f1 = (hom (T,c,c9)) . f2 implies f1 = f2 )
assume that
A3: f1 in Hom (c,c9) and
A4: f2 in Hom (c,c9) ; :: thesis: ( (hom (T,c,c9)) . f1 = (hom (T,c,c9)) . f2 implies f1 = f2 )
A5: f2 is Morphism of c,c9 by A4, Def3;
then A6: T . f2 = (hom (T,c,c9)) . f2 by A3, Th83;
A7: f1 is Morphism of c,c9 by A3, Def3;
then T . f1 = (hom (T,c,c9)) . f1 by A3, Th83;
hence ( (hom (T,c,c9)) . f1 = (hom (T,c,c9)) . f2 implies f1 = f2 ) by A1, A3, A7, A5, A6; :: thesis: verum

end;

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

end;

hence hom (T,c,c9) is one-to-one ; :: thesis: verum

end;

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