let C1, C2 be non empty AltCatStr ; for F being Contravariant FunctorStr over C1,C2 holds
( F is full iff for o1, o2 being Object of C1 holds Morph-Map (F,o2,o1) is onto )
let F be Contravariant FunctorStr over C1,C2; ( F is full iff for o1, o2 being Object of C1 holds Morph-Map (F,o2,o1) is onto )
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 onto ) implies F is full )
assume A1:
F is
full
;
for o1, o2 being Object of C1 holds Morph-Map (F,o2,o1) is onto let o1,
o2 be
Object of
C1;
Morph-Map (F,o2,o1) is onto thus
Morph-Map (
F,
o2,
o1) is
onto
verumproof
A2:
[o2,o1] in [: the carrier of C1, the carrier of C1:]
by ZFMISC_1:87;
then A3:
[o2,o1] in dom the
ObjectMap of
F
by FUNCT_2:def 1;
consider f being
ManySortedFunction of the
Arrows of
C1, the
Arrows of
C2 * the
ObjectMap of
F such that A4:
f = the
MorphMap of
F
and A5:
f is
"onto"
by A1;
rng (f . [o2,o1]) = ( the Arrows of C2 * the ObjectMap of F) . [o2,o1]
by A5, A2;
hence rng (Morph-Map (F,o2,o1)) =
the
Arrows of
C2 . ( the ObjectMap of F . (o2,o1))
by A4, A3, FUNCT_1:13
.=
<^(F . o1),(F . o2)^>
by FUNCTOR0:23
;
FUNCT_2:def 3 verum
end;
end;
assume A6:
for o1, o2 being Object of C1 holds Morph-Map (F,o2,o1) is onto
; F is full
ex I29 being non empty set ex B9 being ManySortedSet of I29 ex f9 being Function of [: the carrier of C1, the carrier of C1:],I29 st
( the ObjectMap of F = f9 & the Arrows of C2 = B9 & the MorphMap of F is ManySortedFunction of the Arrows of C1,B9 * f9 )
by FUNCTOR0:def 3;
then reconsider f = the MorphMap of F as ManySortedFunction of the Arrows of C1, the Arrows of C2 * the ObjectMap of F ;
take
f
; FUNCTOR0:def 32 ( f = the MorphMap of F & f is "onto" )
thus
f = the MorphMap of F
; f is "onto"
let i be set ; MSUALG_3:def 3 ( not i in [: the carrier of C1, the carrier of C1:] or proj2 (f . i) = ( the ObjectMap of F * the Arrows of C2) . i )
assume
i in [: the carrier of C1, the carrier of C1:]
; proj2 (f . i) = ( the ObjectMap of F * the Arrows of C2) . i
then consider o2, o1 being object such that
A7:
( o2 in the carrier of C1 & o1 in the carrier of C1 )
and
A8:
i = [o2,o1]
by ZFMISC_1:84;
reconsider o1 = o1, o2 = o2 as Object of C1 by A7;
[o2,o1] in [: the carrier of C1, the carrier of C1:]
by ZFMISC_1:87;
then A9:
[o2,o1] in dom the ObjectMap of F
by FUNCT_2:def 1;
Morph-Map (F,o2,o1) is onto
by A6;
then rng (Morph-Map (F,o2,o1)) =
the Arrows of C2 . ((F . o1),(F . o2))
.=
the Arrows of C2 . ( the ObjectMap of F . (o2,o1))
by FUNCTOR0:23
.=
( the Arrows of C2 * the ObjectMap of F) . [o2,o1]
by A9, FUNCT_1:13
;
hence
proj2 (f . i) = ( the ObjectMap of F * the Arrows of C2) . i
by A8; verum