theorem :: GLIB_015:20

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