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

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

end;

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 4;
then reconsider f = the MorphMap of F as ManySortedFunction of the Arrows of C1,the Arrows of C2 * the ObjectMap of F ;
assume A5: for o1, o2 being object of C1 holds Morph-Map F,o1,o2 is onto ; :: thesis: F is full
f is "onto"

proof

let i be set ; :: according to MSUALG_3:def 3 :: thesis: ( not i in [:the carrier of C1,the carrier of C1:] or proj2 (f . i) = (the Arrows of C2 * the ObjectMap of F) . i )
assume i in [:the carrier of C1,the carrier of C1:] ; :: thesis: proj2 (f . i) = (the Arrows of C2 * the ObjectMap of F) . i
then consider o1, o2 being set such that
A6: ( o1 in the carrier of C1 & o2 in the carrier of C1 ) and
A7: i = [o1,o2] by ZFMISC_1:103;
reconsider o1 = o1, o2 = o2 as object of C1 by A6;
[o1,o2] in [:the carrier of C1,the carrier of C1:] by ZFMISC_1:106;
then A8: [o1,o2] in dom the ObjectMap of F by FUNCT_2:def 1;
Morph-Map F,o1,o2 is onto by A5;
then rng (Morph-Map F,o1,o2) = <^(F . o1),(F . o2)^> by FUNCT_2:def 3
.= the Arrows of C2 . (F . o1),(F . o2) by ALTCAT_1:def 2
.= the Arrows of C2 . (the ObjectMap of F . o1,o2) by FUNCTOR0:23
.= (the Arrows of C2 * the ObjectMap of F) . o1,o2 by A8, FUNCT_1:23 ;
hence proj2 (f . i) = (the Arrows of C2 * the ObjectMap of F) . i by A7; :: thesis: verum

end;

hence ex f being ManySortedFunction of the Arrows of C1,the Arrows of C2 * the ObjectMap of F st
( f = the MorphMap of F & f is "onto" ) ; :: according to FUNCTOR0:def 33 :: thesis: verum