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