for G1, G2 being _Graph
for F being non empty PGraphMapping of G1,G2 holds
( the_Vertices_of (dom F) = dom (F _V) & the_Edges_of (dom F) = dom (F _E) & the_Vertices_of (rng F) = rng (F _V) & the_Edges_of (rng F) = rng (F _E) )