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 onto & G is onto holds

G * F is onto

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 onto & G is onto holds

G * F is onto

let F be feasible FunctorStr over C1,C2; :: thesis: for G being FunctorStr over C2,C3 st F is onto & G is onto holds

G * F is onto

let G be FunctorStr over C2,C3; :: thesis: ( F is onto & G is onto implies G * F is onto )

assume that

A1: F is onto and

A2: G is onto ; :: thesis: G * F is onto

set CC3 = [: the carrier of C3, the carrier of C3:];

set CC2 = [: 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:] ;

OMG is onto by A2;

then A3: rng OMG = [: the carrier of C3, the carrier of C3:] by FUNCT_2:def 3;

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

OMF is onto by A1;

then rng OMF = [: the carrier of C2, the carrier of C2:] by FUNCT_2:def 3;

then rng (OMG * OMF) = [: the carrier of C3, the carrier of C3:] by A3, FUNCT_2:14;

then OMG * OMF is onto by FUNCT_2:def 3;

hence the ObjectMap of (G * F) is onto by FUNCTOR0:def 36; :: according to FUNCTOR0:def 7 :: thesis: verum

for F being feasible FunctorStr over C1,C2

for G being FunctorStr over C2,C3 st F is onto & G is onto holds

G * F is onto

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 onto & G is onto holds

G * F is onto

let F be feasible FunctorStr over C1,C2; :: thesis: for G being FunctorStr over C2,C3 st F is onto & G is onto holds

G * F is onto

let G be FunctorStr over C2,C3; :: thesis: ( F is onto & G is onto implies G * F is onto )

assume that

A1: F is onto and

A2: G is onto ; :: thesis: G * F is onto

set CC3 = [: the carrier of C3, the carrier of C3:];

set CC2 = [: 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:] ;

OMG is onto by A2;

then A3: rng OMG = [: the carrier of C3, the carrier of C3:] by FUNCT_2:def 3;

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

OMF is onto by A1;

then rng OMF = [: the carrier of C2, the carrier of C2:] by FUNCT_2:def 3;

then rng (OMG * OMF) = [: the carrier of C3, the carrier of C3:] by A3, FUNCT_2:14;

then OMG * OMF is onto by FUNCT_2:def 3;

hence the ObjectMap of (G * F) is onto by FUNCTOR0:def 36; :: according to FUNCTOR0:def 7 :: thesis: verum