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 A1: ( F is onto & G is onto ) ; :: thesis: G * F is onto
set CC1 = [:the carrier of C1,the carrier of C1:];
set CC2 = [:the carrier of C2,the carrier of C2:];
set CC3 = [:the carrier of C3,the carrier of C3:];
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:] ;
A2: OMF is onto by A1, FUNCTOR0:def 8;
A3: OMG is onto by A1, FUNCTOR0:def 8;
A4: rng OMF = [:the carrier of C2,the carrier of C2:] by A2, FUNCT_2:def 3;
rng OMG = [:the carrier of C3,the carrier of C3:] by A3, FUNCT_2:def 3;
then rng (OMG * OMF) = [:the carrier of C3,the carrier of C3:] by A4, 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