for G1, G2 being _Graph
for H being Subgraph of G2
for F being PGraphMapping of G1,G2 holds
( rng ((H |` F) _V) = (rng (F _V)) /\ (the_Vertices_of H) & rng ((H |` F) _E) = (rng (F _E)) /\ (the_Edges_of H) ) by RELAT_1:88;