theorem Th105: :: GLIB_010:105

for G1, G2, G3 being _Graph
for F1 being PGraphMapping of G1,G2
for F2 being PGraphMapping of G2,G3 st F2 is onto & dom (F2 _V) c= rng (F1 _V) & dom (F2 _E) c= rng (F1 _E) holds
F2 * F1 is onto by RELAT_1:28;