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 ;
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 ;
A9: OMF . i in [: the carrier of C2, the carrier of C2:] by ;
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 ; :: 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 ;
then dom MMGI = ( the Arrows of C2 * OMF) . i by
.= 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 ;
then rng (MMGF . i) = rng (((MMG * OMF) . i) * (MMF . i)) by
.= rng (MMG . (OMF . i)) by
.= ( the Arrows of C3 * the ObjectMap of G) . (OMF . i) by A6, A9
.= the Arrows of C3 . (OMG . (OMF . i)) by
.= the Arrows of C3 . ((OMG * OMF) . i) by
.= 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 ;
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