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 A1: ( F is full & G is full ) ; :: thesis: G * F is full
set CC1 = [:the carrier of C1,the carrier of C1:];
set CC2 = [:the carrier of C2,the carrier of C2:];
set CC3 = [: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
A2: ( MMF = the MorphMap of F & 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
A3: ( MMG = the MorphMap of G & MMG is "onto" ) by A1, FUNCTOR0:def 33;
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:] ;
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;
A4: MMGF = (MMG * OMF) ** MMF by A2, A3, FUNCTOR0:def 37;
take MMGF ; :: thesis: ( MMGF = the MorphMap of (G * F) & MMGF is "onto" )
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 A5: 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 A6: OMF . i in [:the carrier of C2,the carrier of C2:] by FUNCT_2:7;
A7: i in dom ((MMG * OMF) ** MMF) by A5, PARTFUN1:def 4;
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 A6, PBOOLE:def 18;
A8: rng ((MMG . (OMF . i)) * (MMF . i)) = rng (MMG . (OMF . i))

proof

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

suppose A9: 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 A9, RELAT_1:64; :: thesis: verum

end;

suppose A10: 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 A3, A6, MSUALG_3:def 3;
then A11: dom MMGI = the Arrows of C2 . (OMF . i) by A10, FUNCT_2:def 1;
rng ((MMG . (OMF . i)) * (MMF . i)) = rng (MMG . (OMF . i))

proof

dom MMGI = (the Arrows of C2 * OMF) . i by A5, A11, FUNCT_2:21
.= rng (MMF . i) by A2, A5, MSUALG_3:def 3 ;
hence rng ((MMG . (OMF . i)) * (MMF . i)) = rng (MMG . (OMF . i)) by RELAT_1:47; :: thesis: verum

end;

hence rng ((MMG . (OMF . i)) * (MMF . i)) = rng (MMG . (OMF . i)) ; :: thesis: verum

end;

end;

end;

rng (MMGF . i) = rng (((MMG * OMF) . i) * (MMF . i)) by A4, A7, PBOOLE:def 24
.= rng (MMG . (OMF . i)) by A5, A8, FUNCT_2:21
.= (the Arrows of C3 * the ObjectMap of G) . (OMF . i) by A3, A6, MSUALG_3:def 3
.= the Arrows of C3 . (OMG . (OMF . i)) by A5, FUNCT_2:7, FUNCT_2:21
.= the Arrows of C3 . ((OMG * OMF) . i) by A5, 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 A5, 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