let C1 be non empty AltGraph ; :: thesis: for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3 st F is full & G is full holds
G * F is full
let C2, C3 be non empty reflexive AltGraph ; :: thesis: for F being feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3 st F is full & G is full holds
G * F is full
let F be feasible FunctorStr over C1,C2; :: thesis: for G being FunctorStr over C2,C3 st F is full & G is full holds
G * F is full
let G be FunctorStr over C2,C3; :: thesis: ( F is full & G is full implies G * F is full )
assume that
A1: F is full and
A2: G is full ; :: thesis: G * F is full
set CC3 = [: the carrier of C3, the carrier of C3:];
set CC2 = [: the carrier of C2, the carrier of C2:];
set CC1 = [: the carrier of C1, the carrier of C1:];
reconsider OMF = the ObjectMap of F as Function of [: the carrier of C1, the carrier of C1:],[: the carrier of C2, the carrier of C2:] ;
reconsider OMG = the ObjectMap of G as Function of [: the carrier of C2, the carrier of C2:],[: the carrier of C3, the carrier of C3:] ;
consider MMF being ManySortedFunction of the Arrows of C1, the Arrows of C2 * the ObjectMap of F such that
A3: MMF = the MorphMap of F and
A4: MMF is "onto" by A1;
consider MMG being ManySortedFunction of the Arrows of C2, the Arrows of C3 * the ObjectMap of G such that
A5: MMG = the MorphMap of G and
A6: MMG is "onto" by A2;
ex f being ManySortedFunction of the Arrows of C1, the Arrows of C3 * the ObjectMap of (G * F) st
( f = the MorphMap of (G * F) & f is "onto" )

proof

reconsider MMGF = the MorphMap of (G * F) as ManySortedFunction of the Arrows of C1, the Arrows of C3 * the ObjectMap of (G * F) by FUNCTOR0:def 4;
take MMGF ; :: thesis: ( MMGF = the MorphMap of (G * F) & MMGF is "onto" )
A7: MMGF = (MMG * OMF) ** MMF by A3, A5, FUNCTOR0:def 36;
for i being set st i in [: the carrier of C1, the carrier of C1:] holds
rng (MMGF . i) = ( the Arrows of C3 * the ObjectMap of (G * F)) . i

proof

let i be set ; :: thesis: ( i in [: the carrier of C1, the carrier of C1:] implies rng (MMGF . i) = ( the Arrows of C3 * the ObjectMap of (G * F)) . i )
assume A8: i in [: the carrier of C1, the carrier of C1:] ; :: thesis: rng (MMGF . i) = ( the Arrows of C3 * the ObjectMap of (G * F)) . i
then reconsider MMGI = MMG . (OMF . i) as Function of ( the Arrows of C2 . (OMF . i)),(( the Arrows of C3 * the ObjectMap of G) . (OMF . i)) by FUNCT_2:5, PBOOLE:def 15;
A9: OMF . i in [: the carrier of C2, the carrier of C2:] by A8, FUNCT_2:5;
A10: rng ((MMG . (OMF . i)) * (MMF . i)) = rng (MMG . (OMF . i))

proof

per cases ( rng MMGI = {} or rng MMGI <> {} ) ;

suppose A11: rng MMGI = {} ; :: thesis: rng ((MMG . (OMF . i)) * (MMF . i)) = rng (MMG . (OMF . i))

rng ({} * (MMF . i)) = {} ;
hence rng ((MMG . (OMF . i)) * (MMF . i)) = rng (MMG . (OMF . i)) by A11, RELAT_1:41; :: thesis: verum

end;

suppose A12: rng MMGI <> {} ; :: thesis: rng ((MMG . (OMF . i)) * (MMF . i)) = rng (MMG . (OMF . i))

rng MMGI = ( the Arrows of C3 * the ObjectMap of G) . (OMF . i) by A6, A9;
then dom MMGI = the Arrows of C2 . (OMF . i) by A12, FUNCT_2:def 1;
then dom MMGI = ( the Arrows of C2 * OMF) . i by A8, FUNCT_2:15
.= rng (MMF . i) by A4, A8 ;
hence rng ((MMG . (OMF . i)) * (MMF . i)) = rng (MMG . (OMF . i)) by RELAT_1:28; :: thesis: verum

end;

end;

end;

i in dom ((MMG * OMF) ** MMF) by A8, PARTFUN1:def 2;
then rng (MMGF . i) = rng (((MMG * OMF) . i) * (MMF . i)) by A7, PBOOLE:def 19
.= rng (MMG . (OMF . i)) by A8, A10, FUNCT_2:15
.= ( the Arrows of C3 * the ObjectMap of G) . (OMF . i) by A6, A9
.= the Arrows of C3 . (OMG . (OMF . i)) by A8, FUNCT_2:5, FUNCT_2:15
.= the Arrows of C3 . ((OMG * OMF) . i) by A8, FUNCT_2:15
.= the Arrows of C3 . ( the ObjectMap of (G * F) . i) by FUNCTOR0:def 36
.= ( the Arrows of C3 * the ObjectMap of (G * F)) . i by A8, FUNCT_2:15 ;
hence rng (MMGF . i) = ( the Arrows of C3 * the ObjectMap of (G * F)) . i ; :: thesis: verum

end;

hence ( MMGF = the MorphMap of (G * F) & MMGF is "onto" ) ; :: thesis: verum

end;

hence G * F is full ; :: thesis: verum