let G1 be non _trivial _Graph; :: thesis:
let W be Walk of G1; :: thesis:
let v be Vertex of G1; :: thesis:
let G2 be removeVertex of G1,v; :: thesis:
assume A1: not v in W .vertices() ; :: thesis:
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:

let y be object ; :: thesis:
assume y in rng W ; :: thesis:
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:

per cases ;

suppose A6: x is odd ; :: thesis:

A7: now :: thesis:

assume y in {v} ; :: thesis:
then not y in W .vertices() by A1, TARSKI:def 1;
hence contradiction by A4, A5, A6, Lm45; :: thesis:

end;

y in the_Vertices_of G1 by A4, A5, A6, Lm1;
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:

end;

suppose x is even ; :: thesis:

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;

A14: now :: thesis:

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

now :: thesis:

per cases by A15, XBOOLE_0:def 3;

suppose y in v .edgesIn() ; :: thesis:

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:

end;

suppose y in v .edgesOut() ; :: thesis:

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:

end;

end;

end;

then ( v = W .vertexAt xaa1 or v = W .vertexAt (x + 1) ) by A13, A12, Def8;
hence contradiction by A1, A13, A12, Th87; :: thesis:

end;

y in the_Edges_of G1 by A4, A11, GLIB_000:def 13;
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:

end;

end;

end;

then y in (the_Vertices_of G2) \/ ((the_Edges_of G1) \ (v .edgesInOut())) by GLIB_000:47;
hence y in (the_Vertices_of G2) \/ (the_Edges_of G2) by A2, GLIB_000:47; :: thesis:

end;

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

now :: thesis:

reconsider lenW2 = len W2 as odd Element of NAT ;
thus len W2 is odd ; :: thesis:
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:
let n be odd Element of NAT ; :: thesis:
assume A17: n < len W2 ; :: thesis:
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:

end;

hence W is Walk of G2 by Def3; :: thesis: