theorem Th164: :: GLIB_010:164

for G1, G2 being _Graph
for G3 being removeLoops of G1
for G4 being removeLoops of G2
for F0 being one-to-one PGraphMapping of G1,G2 ex F being one-to-one PGraphMapping of G3,G4 st
( F = F0 | G3 & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is directed implies F is directed ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) )