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 A1: F is faithful ; :: thesis: for o1, o2 being object of C1 holds Morph-Map F,o1,o2 is one-to-one
let o1, o2 be object of C1; :: thesis: Morph-Map F,o1,o2 is one-to-one
A2: the MorphMap of F is "1-1" by A1, FUNCTOR0:def 31;
A3: [o1,o2] in [:the carrier of C1,the carrier of C1:] by ZFMISC_1:106;
dom the MorphMap of F = [:the carrier of C1,the carrier of C1:] by PARTFUN1:def 4;
hence Morph-Map F,o1,o2 is one-to-one by A2, A3, MSUALG_3:def 2; :: thesis: verum

end;

assume A4: 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 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 A5: ( i in dom the MorphMap of F & 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
A6: ( o1 in the carrier of C1 & o2 in the carrier of C1 & i = [o1,o2] ) by A5, ZFMISC_1:103;
reconsider o1 = o1, o2 = o2 as object of C1 by A6;
the MorphMap of F . o1,o2 = Morph-Map F,o1,o2 ;
hence f is one-to-one by A4, A5, A6; :: thesis: verum