let C1, C2 be non empty AltCatStr ; :: thesis: for F being Covariant FunctorStr of 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 of 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" by FUNCTOR0:def 31;
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 4, ZFMISC_1:106;
hence Morph-Map F,o1,o2 is one-to-one by A1, MSUALG_3:def 2; :: 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 31 :: thesis: for b₁ being set holds
( not i in proj1 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 proj1 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 4;
then consider o1, o2 being set such that
A5: ( o1 in the carrier of C1 & o2 in the carrier of C1 ) and
A6: i = [o1,o2] by A3, ZFMISC_1:103;
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