let C1 be non empty AltGraph ; :: thesis: for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr of C1,C2
for G being FunctorStr of 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 of C1,C2
for G being FunctorStr of C2,C3 st F is full & G is full holds
G * F is full
let F be feasible FunctorStr of C1,C2; :: thesis: for G being FunctorStr of C2,C3 st F is full & G is full holds
G * F is full
let G be FunctorStr of 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, FUNCTOR0:def 33;
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, FUNCTOR0:def 33;
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 5;
take MMGF ; :: thesis: ( MMGF = the MorphMap of (G * F) & MMGF is "onto" )
A7: MMGF = (MMG * OMF) ** MMF by A3, A5, FUNCTOR0:def 37;
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:7, PBOOLE:def 18;
A9: OMF . i in [:the carrier of C2,the carrier of C2:] by A8, FUNCT_2:7;
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:64; :: 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, MSUALG_3:def 3;
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:21
.= rng (MMF . i) by A4, A8, MSUALG_3:def 3 ;
hence rng ((MMG . (OMF . i)) * (MMF . i)) = rng (MMG . (OMF . i)) by RELAT_1:47; :: thesis: verum

end;

end;

end;

i in dom ((MMG * OMF) ** MMF) by A8, PARTFUN1:def 4;
then rng (MMGF . i) = rng (((MMG * OMF) . i) * (MMF . i)) by A7, PBOOLE:def 24
.= rng (MMG . (OMF . i)) by A8, A10, FUNCT_2:21
.= (the Arrows of C3 * the ObjectMap of G) . (OMF . i) by A6, A9, MSUALG_3:def 3
.= the Arrows of C3 . (OMG . (OMF . i)) by A8, FUNCT_2:7, FUNCT_2:21
.= the Arrows of C3 . ((OMG * OMF) . i) by A8, FUNCT_2:21
.= the Arrows of C3 . (the ObjectMap of (G * F) . i) by FUNCTOR0:def 37
.= (the Arrows of C3 * the ObjectMap of (G * F)) . i by A8, FUNCT_2:21 ;
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" ) by MSUALG_3:def 3; :: thesis: verum

end;

hence G * F is full by FUNCTOR0:def 33; :: thesis: verum