theorem :: GLIB_015:23

for G being _Graph
for E being one-to-one ManySortedSet of the_Edges_of G
for W2 being Walk of replaceEdges E ex W1 being Walk of G st
( W1 .vertexSeq() = W2 .vertexSeq() & E * (W1 .edgeSeq()) = W2 .edgeSeq() )