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