theorem Th132: :: GLIB_010:132

for G1, G2 being _Graph
for F being non empty PGraphMapping of G1,G2
for W1 being b₃ -defined Walk of G1
for v, w being object st W1 is_Walk_from v,w holds
F .: W1 is_Walk_from (F _V) . v,(F _V) . w