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