theorem :: GLIB_015:22

for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G
for W2 being Walk of replaceVertices V ex W1 being Walk of G st
( V * (W1 .vertexSeq()) = W2 .vertexSeq() & W1 .edgeSeq() = W2 .edgeSeq() )