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 onto & G is onto holds
G * F is onto
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 onto & G is onto holds
G * F is onto
let F be feasible FunctorStr of C1,C2; :: thesis: for G being FunctorStr of C2,C3 st F is onto & G is onto holds
G * F is onto
let G be FunctorStr of 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, FUNCTOR0:def 8;
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, FUNCTOR0:def 8;
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:20;
then OMG * OMF is onto by FUNCT_2:def 3;
hence the ObjectMap of (G * F) is onto by FUNCTOR0:def 37; :: according to FUNCTOR0:def 8 :: thesis: verum