theorem :: GLIB_015:19

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