theorem Th6: :: GLIB_010:6

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