let G1, G2, G3 be _Graph; :: thesis: for F1 being PGraphMapping of G1,G2

for F2 being PGraphMapping of G2,G3 st F1 is onto & F2 is onto holds

F2 * F1 is onto

let F1 be PGraphMapping of G1,G2; :: thesis: for F2 being PGraphMapping of G2,G3 st F1 is onto & F2 is onto holds

F2 * F1 is onto

let F2 be PGraphMapping of G2,G3; :: thesis: ( F1 is onto & F2 is onto implies F2 * F1 is onto )

assume A1: ( F1 is onto & F2 is onto ) ; :: thesis: F2 * F1 is onto

then ( dom (F2 _V) c= rng (F1 _V) & dom (F2 _E) c= rng (F1 _E) ) ;

hence F2 * F1 is onto by A1, Th105; :: thesis: verum

for F2 being PGraphMapping of G2,G3 st F1 is onto & F2 is onto holds

F2 * F1 is onto

let F1 be PGraphMapping of G1,G2; :: thesis: for F2 being PGraphMapping of G2,G3 st F1 is onto & F2 is onto holds

F2 * F1 is onto

let F2 be PGraphMapping of G2,G3; :: thesis: ( F1 is onto & F2 is onto implies F2 * F1 is onto )

assume A1: ( F1 is onto & F2 is onto ) ; :: thesis: F2 * F1 is onto

then ( dom (F2 _V) c= rng (F1 _V) & dom (F2 _E) c= rng (F1 _E) ) ;

hence F2 * F1 is onto by A1, Th105; :: thesis: verum