let G1 be _Graph; :: thesis: for G2 being removeDParallelEdges of G1
for W1 being Walk of G1 ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last()
let G2 be removeDParallelEdges of G1; :: thesis: for W1 being Walk of G1 ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last()
let W1 be Walk of G1; :: thesis: ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last()
consider W2 being Walk of G2 such that
A1: W1 .vertexSeq() = W2 .vertexSeq() by Th99;
take W2 ; :: thesis: W2 is_Walk_from W1 .first() ,W1 .last()
thus W2 is_Walk_from W1 .first() ,W1 .last() by A1, Th30; :: thesis: verum