theorem Th21: :: GLIB_015:21

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