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 = () \ ();
set W2 = W;
set VG2 = () \ {v};
v .edgesInOut() = G1 .edgesInOut {v} by GLIB_000:def 40;
then A2: (the_Edges_of G1) \ () = G1 .edgesBetween (() \ {v}) by GLIB_000:35;
now :: thesis: for y being object st y in rng W holds
y in () \/ ()
let y be object ; :: thesis: ( y in rng W implies y in () \/ () )
assume y in rng W ; :: thesis: y in () \/ ()
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 ;
now :: thesis: y in (() \ {v}) \/ (() \ ())
per cases ( x is odd or x is even ) ;
suppose A6: x is odd ; :: thesis: y in (() \ {v}) \/ (() \ ())
y in the_Vertices_of G1 by A4, A5, A6, Lm1;
then y in () \ {v} by ;
hence y in (() \ {v}) \/ (() \ ()) by XBOOLE_0:def 3; :: thesis: verum
end;
suppose x is even ; :: thesis: y in (() \ {v}) \/ (() \ ())
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 ;
A12: x + 1 <= len W by ;
A13: xaa1 <= len W by ;
A14: now :: thesis: not y in v .edgesInOut()
assume y in v .edgesInOut() ; :: thesis: contradiction
then A15: y in () \/ () by GLIB_000:60;
now :: thesis: ( v = W . xaa1 or v = W . (x + 1) )
per cases by ;
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 ; :: thesis: verum
end;
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 ; :: thesis: verum
end;
end;
end;
then ( v = W .vertexAt xaa1 or v = W .vertexAt (x + 1) ) by ;
hence contradiction by A1, A13, A12, Th87; :: thesis: verum
end;
y in the_Edges_of G1 by ;
then y in () \ () by ;
hence y in (() \ {v}) \/ (() \ ()) by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
then y in () \/ (() \ ()) by GLIB_000:47;
hence y in () \/ () by ; :: thesis: verum
end;
then rng W c= () \/ () by TARSKI:def 3;
then reconsider W2 = W as FinSequence of () \/ () 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 ) )
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 ;
W .first() in the_Vertices_of G1 ;
then W2 . 1 in () \ {v} by ;
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 ;
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 ;
W . n <> v by ;
then not W . (n + 1) in v .edgesInOut() by ;
then W . (n + 1) in () \ () by ;
then W . (n + 1) in the_Edges_of G2 by ;
hence W . (n + 1) Joins W . n,W . (n + 2),G2 by ; :: thesis: verum
end;
hence W is Walk of G2 by Def3; :: thesis: verum