let G be _Graph; :: thesis: 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 W2 being Walk of replaceVerticesEdges (V,E) ex W1 being Walk of G 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; :: thesis: for E being one-to-one ManySortedSet of the_Edges_of G
for W2 being Walk of replaceVerticesEdges (V,E) ex W1 being Walk of G st
( V * (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 replaceVerticesEdges (V,E) ex W1 being Walk of G 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 one-to-one PGraphMapping of G, replaceVerticesEdges (V,E) by A1;
let W2 be Walk of replaceVerticesEdges (V,E); :: thesis: ex W1 being Walk of G st
( V * (W1 .vertexSeq()) = W2 .vertexSeq() & E * (W1 .edgeSeq()) = W2 .edgeSeq() )
reconsider W2 = W2 as F -valued Walk of replaceVerticesEdges (V,E) by A1, GLIB_010:122;
take F " W2 ; :: thesis: ( V * ((F " W2) .vertexSeq()) = W2 .vertexSeq() & E * ((F " W2) .edgeSeq()) = W2 .edgeSeq() )
thus ( V * ((F " W2) .vertexSeq()) = W2 .vertexSeq() & E * ((F " W2) .edgeSeq()) = W2 .edgeSeq() ) by A1, GLIB_010:def 39; :: thesis: verum