theorem Th5: :: GLIB_010:5

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for e being object st e in dom (F _E) holds
( (the_Source_of G1) . e in dom (F _V) & (the_Target_of G1) . e in dom (F _V) )