set VE = (the_Vertices_of G) \/ (the_Edges_of G);

set W = <*v*>;

set v9 = v;

reconsider v9 = v as Element of (the_Vertices_of G) \/ (the_Edges_of G) by XBOOLE_0:def 3;

<*v9*> is FinSequence of (the_Vertices_of G) \/ (the_Edges_of G) ;

then reconsider W = <*v*> as FinSequence of (the_Vertices_of G) \/ (the_Edges_of G) ;

set W = <*v*>;

set v9 = v;

reconsider v9 = v as Element of (the_Vertices_of G) \/ (the_Edges_of G) by XBOOLE_0:def 3;

<*v9*> is FinSequence of (the_Vertices_of G) \/ (the_Edges_of G) ;

then reconsider W = <*v*> as FinSequence of (the_Vertices_of G) \/ (the_Edges_of G) ;

now :: thesis: ( len W is odd & W . 1 in the_Vertices_of G & ( for n being odd Element of NAT st n < len <*v*> holds

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

hence
<*v*> is Walk of G
by Def3; :: thesis: verumW . (n + 1) Joins W . n,W . (n + 2),G ) )

thus
len W is odd
by FINSEQ_1:40, JORDAN12:2; :: thesis: ( W . 1 in the_Vertices_of G & ( for n being odd Element of NAT st n < len <*v*> holds

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

W . 1 = v by FINSEQ_1:40;

hence W . 1 in the_Vertices_of G ; :: thesis: for n being odd Element of NAT st n < len <*v*> holds

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

let n be odd Element of NAT ; :: thesis: ( n < len <*v*> implies W . (n + 1) Joins W . n,W . (n + 2),G )

A1: 1 <= n by ABIAN:12;

assume n < len <*v*> ; :: thesis: W . (n + 1) Joins W . n,W . (n + 2),G

hence W . (n + 1) Joins W . n,W . (n + 2),G by A1, FINSEQ_1:40; :: thesis: verum

end;W . (n + 1) Joins W . n,W . (n + 2),G ) )

W . 1 = v by FINSEQ_1:40;

hence W . 1 in the_Vertices_of G ; :: thesis: for n being odd Element of NAT st n < len <*v*> holds

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

let n be odd Element of NAT ; :: thesis: ( n < len <*v*> implies W . (n + 1) Joins W . n,W . (n + 2),G )

A1: 1 <= n by ABIAN:12;

assume n < len <*v*> ; :: thesis: W . (n + 1) Joins W . n,W . (n + 2),G

hence W . (n + 1) Joins W . n,W . (n + 2),G by A1, FINSEQ_1:40; :: thesis: verum