let C1, C2 be non empty AltCatStr ; :: thesis: for F being Contravariant FunctorStr over C1,C2 holds

( F is faithful iff for o1, o2 being Object of C1 holds Morph-Map (F,o2,o1) is one-to-one )

let F be Contravariant FunctorStr over C1,C2; :: thesis: ( F is faithful iff for o1, o2 being Object of C1 holds Morph-Map (F,o2,o1) is one-to-one )

set I = [: the carrier of C1, the carrier of C1:];

let i be set ; :: according to FUNCTOR0:def 30,MSUALG_3:def 2 :: thesis: for b_{1} being set holds

( not i in proj1 the MorphMap of F or not the MorphMap of F . i = b_{1} or b_{1} 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 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

( F is faithful iff for o1, o2 being Object of C1 holds Morph-Map (F,o2,o1) is one-to-one )

let F be Contravariant FunctorStr over C1,C2; :: thesis: ( F is faithful iff for o1, o2 being Object of C1 holds Morph-Map (F,o2,o1) 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,o2,o1) is one-to-one ) implies F is faithful )

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

then A1: the MorphMap of F is "1-1" ;

let o1, o2 be Object of C1; :: thesis: Morph-Map (F,o2,o1) is one-to-one

( [o2,o1] 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,o2,o1) is one-to-one by A1; :: thesis: verum

end;then A1: the MorphMap of F is "1-1" ;

let o1, o2 be Object of C1; :: thesis: Morph-Map (F,o2,o1) is one-to-one

( [o2,o1] 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,o2,o1) is one-to-one by A1; :: thesis: verum

let i be set ; :: according to FUNCTOR0:def 30,MSUALG_3:def 2 :: thesis: for b

( not i in proj1 the MorphMap of F or not the MorphMap of F . i = b

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 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