let G be _Graph; :: thesis: 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() )
let V be non empty one-to-one ManySortedSet of the_Vertices_of G; :: thesis: for W2 being Walk of replaceVertices V ex W1 being Walk of G st
( V * (W1 .vertexSeq()) = W2 .vertexSeq() & W1 .edgeSeq() = W2 .edgeSeq() )
let W2 be Walk of replaceVertices V; :: thesis: ex W1 being Walk of G st
( V * (W1 .vertexSeq()) = W2 .vertexSeq() & W1 .edgeSeq() = W2 .edgeSeq() )
consider W1 being Walk of G such that
A1: V * (W1 .vertexSeq()) = W2 .vertexSeq() and
A2: (id (the_Edges_of G)) * (W1 .edgeSeq()) = W2 .edgeSeq() by Th21;
take W1 ; :: thesis: ( V * (W1 .vertexSeq()) = W2 .vertexSeq() & W1 .edgeSeq() = W2 .edgeSeq() )
rng (W1 .edgeSeq()) c= the_Edges_of G ;
hence ( V * (W1 .vertexSeq()) = W2 .vertexSeq() & W1 .edgeSeq() = W2 .edgeSeq() ) by A1, A2, RELAT_1:53; :: thesis: verum