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_{1}[ Walk of G1] means ex W2 being Walk of G2 st $1 .vertexSeq() = W2 .vertexSeq() ;

A1: for W being V5() Walk of G1 holds S_{1}[W]

for e being object st e in (W .last()) .edgesInOut() & S_{1}[W] holds

S_{1}[W .addEdge e]
_{1}[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

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

A1: for W being V5() Walk of G1 holds S

proof

A3:
for W being Walk of G1
let W be V5() Walk of G1; :: thesis: S_{1}[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;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

for e being object st e in (W .last()) .edgesInOut() & S

S

proof

for W1 being Walk of G1 holds S
let W1 be Walk of G1; :: thesis: for e being object st e in (W1 .last()) .edgesInOut() & S_{1}[W1] holds

S_{1}[W1 .addEdge e]

let e0 be object ; :: thesis: ( e0 in (W1 .last()) .edgesInOut() & S_{1}[W1] implies S_{1}[W1 .addEdge e0] )

assume A4: ( e0 in (W1 .last()) .edgesInOut() & S_{1}[W1] )
; :: thesis: S_{1}[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;

end;S

let e0 be object ; :: thesis: ( e0 in (W1 .last()) .edgesInOut() & S

assume A4: ( e0 in (W1 .last()) .edgesInOut() & S

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;

end;

suppose A9:
(the_Source_of G1) . e0 = W1 .last()
; :: thesis: S_{1}[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;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

suppose A14:
(the_Target_of G1) . e0 = W1 .last()
; :: thesis: S_{1}[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;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

hence for W1 being Walk of G1 ex W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq() ; :: thesis: verum