for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 holds
( F | (dom F) = F & (rng F) |` F = F )