let C1, C2 be non empty AltCatStr ; :: thesis: for F being Covariant FunctorStr over C1,C2 holds
( F is faithful iff for o1, o2 being Object of C1 holds Morph-Map (F,o1,o2) is one-to-one )
let F be Covariant FunctorStr over C1,C2; :: thesis: ( F is faithful iff for o1, o2 being Object of C1 holds Morph-Map (F,o1,o2) is one-to-one )
set I = [: the carrier of C1, the carrier of C1:];

hereby :: thesis: ( ( for o1, o2 being Object of C1 holds Morph-Map (F,o1,o2) is one-to-one ) implies F is faithful )

assume F is faithful ; :: thesis: for o1, o2 being Object of C1 holds Morph-Map (F,o1,o2) is one-to-one
then A1: the MorphMap of F is "1-1" ;
let o1, o2 be Object of C1; :: thesis: Morph-Map (F,o1,o2) is one-to-one
( [o1,o2] in [: the carrier of C1, the carrier of C1:] & dom the MorphMap of F = [: the carrier of C1, the carrier of C1:] ) by PARTFUN1:def 2, ZFMISC_1:87;
hence Morph-Map (F,o1,o2) is one-to-one by A1; :: thesis: verum

end;

assume A2: for o1, o2 being Object of C1 holds Morph-Map (F,o1,o2) is one-to-one ; :: thesis: F is faithful
let i be set ; :: according to MSUALG_3:def 2,FUNCTOR0:def 30 :: thesis: for b₁ being set holds
( not i in dom the MorphMap of F or not the MorphMap of F . i = b₁ or b₁ is one-to-one )
let f be Function; :: thesis: ( not i in dom the MorphMap of F or not the MorphMap of F . i = f or f is one-to-one )
assume that
A3: i in dom the MorphMap of F and
A4: the MorphMap of F . i = f ; :: thesis: f is one-to-one
dom the MorphMap of F = [: the carrier of C1, the carrier of C1:] by PARTFUN1:def 2;
then consider o1, o2 being object such that
A5: ( o1 in the carrier of C1 & o2 in the carrier of C1 ) and
A6: i = [o1,o2] by A3, ZFMISC_1:84;
reconsider o1 = o1, o2 = o2 as Object of C1 by A5;
the MorphMap of F . (o1,o2) = Morph-Map (F,o1,o2) ;
hence f is one-to-one by A2, A4, A6; :: thesis: verum