let G1 be _Graph; :: thesis: for G2 being removeDParallelEdges of G1
for W1 being Walk of G1 ex W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq()
let G2 be removeDParallelEdges of G1; :: thesis: for W1 being Walk of G1 ex W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq()
let W1 be Walk of G1; :: thesis: ex W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq()
set G3 = the removeParallelEdges of G2;
the removeParallelEdges of G2 is removeParallelEdges of G1 by Th95;
then consider W3 being Walk of the removeParallelEdges of G2 such that
A1: W1 .vertexSeq() = W3 .vertexSeq() by Th98;
reconsider W2 = W3 as Walk of G2 by GLIB_001:167;
take W2 ; :: thesis: W1 .vertexSeq() = W2 .vertexSeq()
thus W1 .vertexSeq() = W2 .vertexSeq() by A1, GLIB_001:76; :: thesis: verum