let G be _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 W1 being Walk of G ex W2 being Walk of replaceVerticesEdges (V,E) st
( V * (W1 .vertexSeq()) = W2 .vertexSeq() & E * (W1 .edgeSeq()) = W2 .edgeSeq() )
let V be non empty one-to-one ManySortedSet of the_Vertices_of G; for E being one-to-one ManySortedSet of the_Edges_of G
for W1 being Walk of G ex W2 being Walk of replaceVerticesEdges (V,E) st
( V * (W1 .vertexSeq()) = W2 .vertexSeq() & E * (W1 .edgeSeq()) = W2 .edgeSeq() )
let E be one-to-one ManySortedSet of the_Edges_of G; for W1 being Walk of G ex W2 being Walk of replaceVerticesEdges (V,E) st
( V * (W1 .vertexSeq()) = W2 .vertexSeq() & E * (W1 .edgeSeq()) = W2 .edgeSeq() )
consider F being PGraphMapping of G, replaceVerticesEdges (V,E) such that
A1:
( F _V = V & F _E = E & F is Disomorphism )
by Th16;
reconsider F = F as non empty PGraphMapping of G, replaceVerticesEdges (V,E) by A1;
let W1 be Walk of G; ex W2 being Walk of replaceVerticesEdges (V,E) st
( V * (W1 .vertexSeq()) = W2 .vertexSeq() & E * (W1 .edgeSeq()) = W2 .edgeSeq() )
reconsider W1 = W1 as F -defined Walk of G by A1, GLIB_010:121;
take
F .: W1
; ( V * (W1 .vertexSeq()) = (F .: W1) .vertexSeq() & E * (W1 .edgeSeq()) = (F .: W1) .edgeSeq() )
thus
( V * (W1 .vertexSeq()) = (F .: W1) .vertexSeq() & E * (W1 .edgeSeq()) = (F .: W1) .edgeSeq() )
by A1, GLIB_010:def 37; verum