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