theorem Th122: :: GLIB_010:122

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for W2 being Walk of G2 st F is onto holds
W2 is F -valued ;