let C1, C2 be non empty AltCatStr ; :: thesis: for F being Contravariant FunctorStr of 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 of C1,C2; :: thesis: ( 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 :: thesis: ( ( for o1, o2 being object of C1 holds Morph-Map F,o2,o1 is onto ) implies F is full )

assume A1: F is full ; :: thesis: for o1, o2 being object of C1 holds Morph-Map F,o2,o1 is onto
let o1, o2 be object of C1; :: thesis: Morph-Map F,o2,o1 is onto
thus Morph-Map F,o2,o1 is onto :: thesis: verum

proof

consider f being ManySortedFunction of the Arrows of C1,the Arrows of C2 * the ObjectMap of F such that
A2: ( f = the MorphMap of F & f is "onto" ) by A1, FUNCTOR0:def 33;
A3: [o2,o1] in [:the carrier of C1,the carrier of C1:] by ZFMISC_1:106;
then A4: [o2,o1] in dom the ObjectMap of F by FUNCT_2:def 1;
rng (f . [o2,o1]) = (the Arrows of C2 * the ObjectMap of F) . [o2,o1] by A2, A3, MSUALG_3:def 3;
hence rng (Morph-Map F,o2,o1) = the Arrows of C2 . (the ObjectMap of F . o2,o1) by A2, A4, FUNCT_1:23
.= <^(F . o1),(F . o2)^> by FUNCTOR0:24 ;
:: according to FUNCT_2:def 3 :: thesis: verum

end;

end;

assume A5: for o1, o2 being object of C1 holds Morph-Map F,o2,o1 is onto ; :: thesis: F is full
consider I2' being non empty set , B' being ManySortedSet of , f' being Function of [:the carrier of C1,the carrier of C1:],I2' such that
A6: the ObjectMap of F = f' and
A7: ( the Arrows of C2 = B' & the MorphMap of F is ManySortedFunction of the Arrows of C1,B' * f' ) by FUNCTOR0:def 4;
reconsider f = the MorphMap of F as ManySortedFunction of the Arrows of C1,the Arrows of C2 * the ObjectMap of F by A6, A7;
take f ; :: according to FUNCTOR0:def 33 :: thesis: ( f = the MorphMap of F & f is "onto" )
thus f = the MorphMap of F ; :: thesis: f is "onto"
let i be set ; :: according to MSUALG_3:def 3 :: thesis: ( not i in [:the carrier of C1,the carrier of C1:] or rng (f . i) = (the ObjectMap of F * the Arrows of C2) . i )
assume i in [:the carrier of C1,the carrier of C1:] ; :: thesis: rng (f . i) = (the ObjectMap of F * the Arrows of C2) . i
then consider o2, o1 being set such that
A8: ( o2 in the carrier of C1 & o1 in the carrier of C1 & i = [o2,o1] ) by ZFMISC_1:103;
reconsider o1 = o1, o2 = o2 as object of C1 by A8;
[o2,o1] in [:the carrier of C1,the carrier of C1:] by ZFMISC_1:106;
then A9: [o2,o1] in dom the ObjectMap of F by FUNCT_2:def 1;
Morph-Map F,o2,o1 is onto by A5;
then rng (Morph-Map F,o2,o1) = the Arrows of C2 . (F . o1),(F . o2) by FUNCT_2:def 3
.= the Arrows of C2 . (the ObjectMap of F . o2,o1) by FUNCTOR0:24
.= (the Arrows of C2 * the ObjectMap of F) . [o2,o1] by A9, FUNCT_1:23 ;
hence rng (f . i) = (the ObjectMap of F * the Arrows of C2) . i by A8; :: thesis: verum