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