let C1, C2 be non empty AltCatStr ; :: thesis: for F being Covariant FunctorStr over 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 over 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:];

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

assume A5: for o1, o2 being Object of C1 holds Morph-Map (F,o1,o2) is onto ; :: thesis: F is full

f is "onto"

( f = the MorphMap of F & f is "onto" ) ; :: according to FUNCTOR0:def 32 :: thesis: verum

( F is full iff for o1, o2 being Object of C1 holds Morph-Map (F,o1,o2) is onto )

let F be Covariant FunctorStr over 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 )

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

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:87;

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;

then rng (Morph-Map (F,o1,o2)) = the Arrows of C2 . ( the ObjectMap of F . (o1,o2)) by A1, A4, FUNCT_1:13

.= the Arrows of C2 . ((F . o1),(F . o2)) by FUNCTOR0:22

.= <^(F . o1),(F . o2)^> by ALTCAT_1:def 1 ;

hence Morph-Map (F,o1,o2) is onto by FUNCT_2:def 3; :: thesis: verum

end;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" ;

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:87;

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;

then rng (Morph-Map (F,o1,o2)) = the Arrows of C2 . ( the ObjectMap of F . (o1,o2)) by A1, A4, FUNCT_1:13

.= the Arrows of C2 . ((F . o1),(F . o2)) by FUNCTOR0:22

.= <^(F . o1),(F . o2)^> by ALTCAT_1:def 1 ;

hence Morph-Map (F,o1,o2) is onto by FUNCT_2:def 3; :: thesis: verum

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

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

hence
ex f being ManySortedFunction of the Arrows of C1, the Arrows of C2 * the ObjectMap of F st
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 Arrows of C2 * the ObjectMap of F) . i )

assume i in [: the carrier of C1, the carrier of C1:] ; :: thesis: rng (f . i) = ( the Arrows of C2 * the ObjectMap of F) . i

then consider o1, o2 being object such that

A6: ( o1 in the carrier of C1 & o2 in the carrier of C1 ) and

A7: i = [o1,o2] by ZFMISC_1:84;

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:87;

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 1

.= the Arrows of C2 . ( the ObjectMap of F . (o1,o2)) by FUNCTOR0:22

.= ( the Arrows of C2 * the ObjectMap of F) . (o1,o2) by A8, FUNCT_1:13 ;

hence rng (f . i) = ( the Arrows of C2 * the ObjectMap of F) . i by A7; :: thesis: verum

end;assume i in [: the carrier of C1, the carrier of C1:] ; :: thesis: rng (f . i) = ( the Arrows of C2 * the ObjectMap of F) . i

then consider o1, o2 being object such that

A6: ( o1 in the carrier of C1 & o2 in the carrier of C1 ) and

A7: i = [o1,o2] by ZFMISC_1:84;

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:87;

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 1

.= the Arrows of C2 . ( the ObjectMap of F . (o1,o2)) by FUNCTOR0:22

.= ( the Arrows of C2 * the ObjectMap of F) . (o1,o2) by A8, FUNCT_1:13 ;

hence rng (f . i) = ( the Arrows of C2 * the ObjectMap of F) . i by A7; :: thesis: verum

( f = the MorphMap of F & f is "onto" ) ; :: according to FUNCTOR0:def 32 :: thesis: verum