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" )

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

hence
G * F is full
; :: thesis: verum
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

end;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

hence
( MMGF = the MorphMap of (G * F) & MMGF is "onto" )
; :: thesis: verum
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))

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;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
end;

i in dom ((MMG * OMF) ** MMF)
by A8, PARTFUN1:def 2;per cases
( rng MMGI = {} or rng MMGI <> {} )
;

end;

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;hence rng ((MMG . (OMF . i)) * (MMF . i)) = rng (MMG . (OMF . i)) by A11, RELAT_1:41; :: thesis: verum

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;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

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