let G1 be _Graph; :: thesis: for G2 being removeParallelEdges of G1
for W1 being Walk of G1 ex W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq()
let G2 be removeParallelEdges of G1; :: thesis: for W1 being Walk of G1 ex W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq()
defpred S₁[ Walk of G1] means ex W2 being Walk of G2 st $1 .vertexSeq() = W2 .vertexSeq() ;
A1: for W being trivial Walk of G1 holds S₁[W]

proof

let W be trivial Walk of G1; :: thesis: S₁[W]
consider v1 being Vertex of G1 such that
A2: W = G1 .walkOf v1 by GLIB_001:128;
reconsider v2 = v1 as Vertex of G2 by GLIB_000:def 33;
set W2 = G2 .walkOf v2;
take G2 .walkOf v2 ; :: thesis: W .vertexSeq() = (G2 .walkOf v2) .vertexSeq()
thus W .vertexSeq() = <*v1*> by A2, GLIB_001:69
.= (G2 .walkOf v2) .vertexSeq() by GLIB_001:69 ; :: thesis: verum

end;

A3: for W being Walk of G1
for e being object st e in (W .last()) .edgesInOut() & S₁[W] holds
S₁[W .addEdge e]

proof

let W1 be Walk of G1; :: thesis: for e being object st e in (W1 .last()) .edgesInOut() & S₁[W1] holds
S₁[W1 .addEdge e]
let e0 be object ; :: thesis: ( e0 in (W1 .last()) .edgesInOut() & S₁[W1] implies S₁[W1 .addEdge e0] )
assume A4: ( e0 in (W1 .last()) .edgesInOut() & S₁[W1] ) ; :: thesis: S₁[W1 .addEdge e0]
then consider W2 being Walk of G2 such that
A5: W1 .vertexSeq() = W2 .vertexSeq() ;
A6: ( W2 .first() = W1 .first() & W2 .last() = W1 .last() ) by A5, Th30;
consider E being RepEdgeSelection of G1 such that
A7: G2 is inducedSubgraph of G1, the_Vertices_of G1,E by Def7;
( the_Vertices_of G1 c= the_Vertices_of G1 & the_Edges_of G1 = G1 .edgesBetween (the_Vertices_of G1) ) by GLIB_000:34;
then A8: the_Edges_of G2 = E by A7, GLIB_000:def 37;

per cases ( (the_Source_of G1) . e0 = W1 .last() or (the_Target_of G1) . e0 = W1 .last() ) by A4, GLIB_000:61;

suppose A9: (the_Source_of G1) . e0 = W1 .last() ; :: thesis: S₁[W1 .addEdge e0]

set v = W1 .last() ;
set w = (the_Target_of G1) . e0;
A10: e0 Joins W1 .last() ,(the_Target_of G1) . e0,G1 by A4, A9, GLIB_000:def 13;
then consider e being object such that
A11: ( e Joins W1 .last() ,(the_Target_of G1) . e0,G1 & e in E ) and
for e9 being object st e9 Joins W1 .last() ,(the_Target_of G1) . e0,G1 & e9 in E holds
e9 = e by Def5;
set W3 = W1 .addEdge e0;
set W4 = W2 .addEdge e;
take W2 .addEdge e ; :: thesis: (W1 .addEdge e0) .vertexSeq() = (W2 .addEdge e) .vertexSeq()
A12: e Joins W2 .last() ,(the_Target_of G1) . e0,G2 by A8, A6, A11, GLIB_000:73;
A13: ( e is set & e0 is set ) by TARSKI:1;
thus (W1 .addEdge e0) .vertexSeq() = (W1 .vertexSeq()) ^ <*((the_Target_of G1) . e0)*> by A10, A13, GLIB_001:75
.= (W2 .addEdge e) .vertexSeq() by A5, A12, A13, GLIB_001:75 ; :: thesis: verum

end;

suppose A14: (the_Target_of G1) . e0 = W1 .last() ; :: thesis: S₁[W1 .addEdge e0]

set v = W1 .last() ;
set w = (the_Source_of G1) . e0;
A15: e0 Joins W1 .last() ,(the_Source_of G1) . e0,G1 by A4, A14, GLIB_000:def 13;
then consider e being object such that
A16: ( e Joins W1 .last() ,(the_Source_of G1) . e0,G1 & e in E ) and
for e9 being object st e9 Joins W1 .last() ,(the_Source_of G1) . e0,G1 & e9 in E holds
e9 = e by Def5;
set W3 = W1 .addEdge e0;
set W4 = W2 .addEdge e;
take W2 .addEdge e ; :: thesis: (W1 .addEdge e0) .vertexSeq() = (W2 .addEdge e) .vertexSeq()
A17: e Joins W2 .last() ,(the_Source_of G1) . e0,G2 by A8, A6, A16, GLIB_000:73;
A18: ( e is set & e0 is set ) by TARSKI:1;
thus (W1 .addEdge e0) .vertexSeq() = (W1 .vertexSeq()) ^ <*((the_Source_of G1) . e0)*> by A15, A18, GLIB_001:75
.= (W2 .addEdge e) .vertexSeq() by A5, A17, A18, GLIB_001:75 ; :: thesis: verum

end;

end;

end;

for W1 being Walk of G1 holds S₁[W1] from GLIB_009:sch 1(A1, A3);
hence for W1 being Walk of G1 ex W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq() ; :: thesis: verum