let C1, C2 be non empty AltCatStr ; 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; ( 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 ( ( for o1, o2 being Object of C1 holds Morph-Map (F,o2,o1) is one-to-one ) implies F is faithful )
assume
F is
faithful
;
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;
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;
verum
end;
assume A2:
for o1, o2 being Object of C1 holds Morph-Map (F,o2,o1) is one-to-one
; F is faithful
let i be set ; FUNCTOR0:def 30,MSUALG_3:def 2 for b1 being set holds
( not i in proj1 the MorphMap of F or not the MorphMap of F . i = b1 or b1 is one-to-one )
let f be Function; ( 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
; 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; verum