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 A1:
F is
full
;
:: thesis: for o1, o2 being object of C1 holds Morph-Map F,o1,o2 is onto let o1,
o2 be
object of
C1;
:: thesis: Morph-Map F,o1,o2 is onto 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:
[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 A2, 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;
assume A5:
for o1, o2 being object of C1 holds Morph-Map F,o1,o2 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;
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 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
set such that A8:
(
o1 in the
carrier of
C1 &
o2 in the
carrier of
C1 &
i = [o1,o2] )
by ZFMISC_1:103;
reconsider o1 =
o1,
o2 =
o2 as
object of
C1 by A8;
A9:
Morph-Map F,
o1,
o2 is
onto
by A5;
[o1,o2] in [:the carrier of C1,the carrier of C1:]
by ZFMISC_1:106;
then A10:
[o1,o2] in dom the
ObjectMap of
F
by FUNCT_2:def 1;
rng (Morph-Map F,o1,o2) =
<^(F . o1),(F . o2)^>
by A9, 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 A10, FUNCT_1:23
;
hence
rng (f . i) = (the Arrows of C2 * the ObjectMap of F) . i
by A8;
:: 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