let G1 be non trivial _Graph; :: thesis: for W being Walk of G1

for v being Vertex of G1

for G2 being removeVertex of G1,v st not v in W .vertices() holds

W is Walk of G2

let W be Walk of G1; :: thesis: for v being Vertex of G1

for G2 being removeVertex of G1,v st not v in W .vertices() holds

W is Walk of G2

let v be Vertex of G1; :: thesis: for G2 being removeVertex of G1,v st not v in W .vertices() holds

W is Walk of G2

let G2 be removeVertex of G1,v; :: thesis: ( not v in W .vertices() implies W is Walk of G2 )

assume A1: not v in W .vertices() ; :: thesis: W is Walk of G2

set EG2 = (the_Edges_of G1) \ (v .edgesInOut());

set W2 = W;

set VG2 = (the_Vertices_of G1) \ {v};

v .edgesInOut() = G1 .edgesInOut {v} by GLIB_000:def 40;

then A2: (the_Edges_of G1) \ (v .edgesInOut()) = G1 .edgesBetween ((the_Vertices_of G1) \ {v}) by GLIB_000:35;

then reconsider W2 = W as FinSequence of (the_Vertices_of G2) \/ (the_Edges_of G2) by FINSEQ_1:def 4;

for v being Vertex of G1

for G2 being removeVertex of G1,v st not v in W .vertices() holds

W is Walk of G2

let W be Walk of G1; :: thesis: for v being Vertex of G1

for G2 being removeVertex of G1,v st not v in W .vertices() holds

W is Walk of G2

let v be Vertex of G1; :: thesis: for G2 being removeVertex of G1,v st not v in W .vertices() holds

W is Walk of G2

let G2 be removeVertex of G1,v; :: thesis: ( not v in W .vertices() implies W is Walk of G2 )

assume A1: not v in W .vertices() ; :: thesis: W is Walk of G2

set EG2 = (the_Edges_of G1) \ (v .edgesInOut());

set W2 = W;

set VG2 = (the_Vertices_of G1) \ {v};

v .edgesInOut() = G1 .edgesInOut {v} by GLIB_000:def 40;

then A2: (the_Edges_of G1) \ (v .edgesInOut()) = G1 .edgesBetween ((the_Vertices_of G1) \ {v}) by GLIB_000:35;

now :: thesis: for y being object st y in rng W holds

y in (the_Vertices_of G2) \/ (the_Edges_of G2)

then
rng W c= (the_Vertices_of G2) \/ (the_Edges_of G2)
by TARSKI:def 3;y in (the_Vertices_of G2) \/ (the_Edges_of G2)

let y be object ; :: thesis: ( y in rng W implies y in (the_Vertices_of G2) \/ (the_Edges_of G2) )

assume y in rng W ; :: thesis: y in (the_Vertices_of G2) \/ (the_Edges_of G2)

then consider x being object such that

A3: x in dom W and

A4: y = W . x by FUNCT_1:def 3;

reconsider x = x as Element of NAT by A3;

A5: x <= len W by A3, FINSEQ_3:25;

hence y in (the_Vertices_of G2) \/ (the_Edges_of G2) by A2, GLIB_000:47; :: thesis: verum

end;assume y in rng W ; :: thesis: y in (the_Vertices_of G2) \/ (the_Edges_of G2)

then consider x being object such that

A3: x in dom W and

A4: y = W . x by FUNCT_1:def 3;

reconsider x = x as Element of NAT by A3;

A5: x <= len W by A3, FINSEQ_3:25;

now :: thesis: y in ((the_Vertices_of G1) \ {v}) \/ ((the_Edges_of G1) \ (v .edgesInOut()))end;

then
y in (the_Vertices_of G2) \/ ((the_Edges_of G1) \ (v .edgesInOut()))
by GLIB_000:47;per cases
( x is odd or x is even )
;

end;

suppose A6:
x is odd
; :: thesis: y in ((the_Vertices_of G1) \ {v}) \/ ((the_Edges_of G1) \ (v .edgesInOut()))

then y in (the_Vertices_of G1) \ {v} by A7, XBOOLE_0:def 5;

hence y in ((the_Vertices_of G1) \ {v}) \/ ((the_Edges_of G1) \ (v .edgesInOut())) by XBOOLE_0:def 3; :: thesis: verum

end;

A7: now :: thesis: not y in {v}

y in the_Vertices_of G1
by A4, A5, A6, Lm1;assume
y in {v}
; :: thesis: contradiction

then not y in W .vertices() by A1, TARSKI:def 1;

hence contradiction by A4, A5, A6, Lm45; :: thesis: verum

end;then not y in W .vertices() by A1, TARSKI:def 1;

hence contradiction by A4, A5, A6, Lm45; :: thesis: verum

then y in (the_Vertices_of G1) \ {v} by A7, XBOOLE_0:def 5;

hence y in ((the_Vertices_of G1) \ {v}) \/ ((the_Edges_of G1) \ (v .edgesInOut())) by XBOOLE_0:def 3; :: thesis: verum

suppose
x is even
; :: thesis: y in ((the_Vertices_of G1) \ {v}) \/ ((the_Edges_of G1) \ (v .edgesInOut()))

then reconsider x = x as even Element of NAT ;

consider xaa1 being odd Element of NAT such that

A8: xaa1 = x - 1 and

A9: x - 1 in dom W and

A10: x + 1 in dom W and

A11: W . x Joins W . xaa1,W . (x + 1),G1 by A3, Lm2;

A12: x + 1 <= len W by A10, FINSEQ_3:25;

A13: xaa1 <= len W by A8, A9, FINSEQ_3:25;

then y in (the_Edges_of G1) \ (v .edgesInOut()) by A14, XBOOLE_0:def 5;

hence y in ((the_Vertices_of G1) \ {v}) \/ ((the_Edges_of G1) \ (v .edgesInOut())) by XBOOLE_0:def 3; :: thesis: verum

end;consider xaa1 being odd Element of NAT such that

A8: xaa1 = x - 1 and

A9: x - 1 in dom W and

A10: x + 1 in dom W and

A11: W . x Joins W . xaa1,W . (x + 1),G1 by A3, Lm2;

A12: x + 1 <= len W by A10, FINSEQ_3:25;

A13: xaa1 <= len W by A8, A9, FINSEQ_3:25;

A14: now :: thesis: not y in v .edgesInOut()

y in the_Edges_of G1
by A4, A11, GLIB_000:def 13;assume
y in v .edgesInOut()
; :: thesis: contradiction

then A15: y in (v .edgesIn()) \/ (v .edgesOut()) by GLIB_000:60;

hence contradiction by A1, A13, A12, Th87; :: thesis: verum

end;then A15: y in (v .edgesIn()) \/ (v .edgesOut()) by GLIB_000:60;

now :: thesis: ( v = W . xaa1 or v = W . (x + 1) )end;

then
( v = W .vertexAt xaa1 or v = W .vertexAt (x + 1) )
by A13, A12, Def8;per cases
( y in v .edgesIn() or y in v .edgesOut() )
by A15, XBOOLE_0:def 3;

end;

suppose
y in v .edgesIn()
; :: thesis: ( v = W . xaa1 or v = W . (x + 1) )

then
(the_Target_of G1) . y = v
by GLIB_000:56;

hence ( v = W . xaa1 or v = W . (x + 1) ) by A4, A11, GLIB_000:def 13; :: thesis: verum

end;hence ( v = W . xaa1 or v = W . (x + 1) ) by A4, A11, GLIB_000:def 13; :: thesis: verum

suppose
y in v .edgesOut()
; :: thesis: ( v = W . xaa1 or v = W . (x + 1) )

then
(the_Source_of G1) . y = v
by GLIB_000:58;

hence ( v = W . xaa1 or v = W . (x + 1) ) by A4, A11, GLIB_000:def 13; :: thesis: verum

end;hence ( v = W . xaa1 or v = W . (x + 1) ) by A4, A11, GLIB_000:def 13; :: thesis: verum

hence contradiction by A1, A13, A12, Th87; :: thesis: verum

then y in (the_Edges_of G1) \ (v .edgesInOut()) by A14, XBOOLE_0:def 5;

hence y in ((the_Vertices_of G1) \ {v}) \/ ((the_Edges_of G1) \ (v .edgesInOut())) by XBOOLE_0:def 3; :: thesis: verum

hence y in (the_Vertices_of G2) \/ (the_Edges_of G2) by A2, GLIB_000:47; :: thesis: verum

then reconsider W2 = W as FinSequence of (the_Vertices_of G2) \/ (the_Edges_of G2) by FINSEQ_1:def 4;

now :: thesis: ( len W2 is odd & W2 . 1 in the_Vertices_of G2 & ( for n being odd Element of NAT st n < len W2 holds

W . (n + 1) Joins W . n,W . (n + 2),G2 ) )

hence
W is Walk of G2
by Def3; :: thesis: verumW . (n + 1) Joins W . n,W . (n + 2),G2 ) )

reconsider lenW2 = len W2 as odd Element of NAT ;

thus len W2 is odd ; :: thesis: ( W2 . 1 in the_Vertices_of G2 & ( for n being odd Element of NAT st n < len W2 holds

W . (n + 1) Joins W . n,W . (n + 2),G2 ) )

W .first() in W .vertices() by Th86;

then A16: not W2 . 1 in {v} by A1, TARSKI:def 1;

W .first() in the_Vertices_of G1 ;

then W2 . 1 in (the_Vertices_of G1) \ {v} by A16, XBOOLE_0:def 5;

hence W2 . 1 in the_Vertices_of G2 by GLIB_000:47; :: thesis: for n being odd Element of NAT st n < len W2 holds

W . (n + 1) Joins W . n,W . (n + 2),G2

let n be odd Element of NAT ; :: thesis: ( n < len W2 implies W . (n + 1) Joins W . n,W . (n + 2),G2 )

assume A17: n < len W2 ; :: thesis: W . (n + 1) Joins W . n,W . (n + 2),G2

then A18: W . (n + 1) Joins W . n,W . (n + 2),G1 by Def3;

then A19: W . (n + 1) in the_Edges_of G1 by GLIB_000:def 13;

n + 1 <= len W2 by A17, NAT_1:13;

then n + 1 < lenW2 by XXREAL_0:1;

then (n + 1) + 1 <= len W2 by NAT_1:13;

then A20: W . (n + 2) <> v by A1, Lm45;

W . n <> v by A1, A17, Lm45;

then not W . (n + 1) in v .edgesInOut() by A18, A20, GLIB_000:65;

then W . (n + 1) in (the_Edges_of G1) \ (v .edgesInOut()) by A19, XBOOLE_0:def 5;

then W . (n + 1) in the_Edges_of G2 by A2, GLIB_000:47;

hence W . (n + 1) Joins W . n,W . (n + 2),G2 by A18, GLIB_000:73; :: thesis: verum

end;thus len W2 is odd ; :: thesis: ( W2 . 1 in the_Vertices_of G2 & ( for n being odd Element of NAT st n < len W2 holds

W . (n + 1) Joins W . n,W . (n + 2),G2 ) )

W .first() in W .vertices() by Th86;

then A16: not W2 . 1 in {v} by A1, TARSKI:def 1;

W .first() in the_Vertices_of G1 ;

then W2 . 1 in (the_Vertices_of G1) \ {v} by A16, XBOOLE_0:def 5;

hence W2 . 1 in the_Vertices_of G2 by GLIB_000:47; :: thesis: for n being odd Element of NAT st n < len W2 holds

W . (n + 1) Joins W . n,W . (n + 2),G2

let n be odd Element of NAT ; :: thesis: ( n < len W2 implies W . (n + 1) Joins W . n,W . (n + 2),G2 )

assume A17: n < len W2 ; :: thesis: W . (n + 1) Joins W . n,W . (n + 2),G2

then A18: W . (n + 1) Joins W . n,W . (n + 2),G1 by Def3;

then A19: W . (n + 1) in the_Edges_of G1 by GLIB_000:def 13;

n + 1 <= len W2 by A17, NAT_1:13;

then n + 1 < lenW2 by XXREAL_0:1;

then (n + 1) + 1 <= len W2 by NAT_1:13;

then A20: W . (n + 2) <> v by A1, Lm45;

W . n <> v by A1, A17, Lm45;

then not W . (n + 1) in v .edgesInOut() by A18, A20, GLIB_000:65;

then W . (n + 1) in (the_Edges_of G1) \ (v .edgesInOut()) by A19, XBOOLE_0:def 5;

then W . (n + 1) in the_Edges_of G2 by A2, GLIB_000:47;

hence W . (n + 1) Joins W . n,W . (n + 2),G2 by A18, GLIB_000:73; :: thesis: verum