theorem Th97: :: GLIBPRE1:96

for G1, G2 being _Graph
for F being non empty one-to-one PGraphMapping of G1,G2
for W2 being b₃ -valued Walk of G2
for v, w being object st W2 is_Walk_from v,w holds
F " W2 is_Walk_from ((F ") _V) . v,((F ") _V) . w by GLIB_010:132;