for G1, G2 being _Graph
for F being non empty PGraphMapping of G1,G2
for V2 being non empty Subset of (the_Vertices_of (rng F))
for H2 being inducedSubgraph of (rng F),V2
for H1 being inducedSubgraph of G1,((F _V) " (the_Vertices_of H2)) st G1 .edgesBetween ((F _V) " (the_Vertices_of H2)) c= dom (F _E) holds
rng (F | H1) == H2