theorem Th81: :: GLIB_010:81

for G1, G2 being _Graph
for F being non empty one-to-one PGraphMapping of G1,G2 holds
( dom F = rng (F ") & rng F = dom (F ") )