theorem Th112: :: GLIBPRE1:109

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for H being Subgraph of G1
for F9 being PGraphMapping of H, rng (F | H) st F9 = F | H holds
( ( not F9 is empty implies F9 is onto ) & ( F is total implies F9 is total ) & ( F is one-to-one implies F9 is one-to-one ) & ( F is directed implies F9 is directed ) & ( F is semi-continuous implies F9 is semi-continuous ) & ( F is continuous & F _E is one-to-one implies F9 is continuous ) & ( F is semi-Dcontinuous implies F9 is semi-Dcontinuous ) & ( F is Dcontinuous & F _E is one-to-one implies F9 is Dcontinuous ) )