for G3, G4 being _Graph
for V1, V2 being set
for G1 being addVertices of G3,V1
for G2 being addVertices of G4,V2
for F0 being PGraphMapping of G3,G4
for f being one-to-one Function st dom f = V1 \ (the_Vertices_of G3) & rng f = V2 \ (the_Vertices_of G4) holds
ex F being PGraphMapping of G1,G2 st
( F = [((F0 _V) +* f),(F0 _E)] & ( not F0 is empty implies not F is empty ) & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) )