theorem :: GLIBPRE1:88

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 holds F is PGraphMapping of G1, rng F