set VE = (the_Vertices_of G) \/ (the_Edges_of G);
set W = <*v*>;
set v' = v;
reconsider v' = v as Element of (the_Vertices_of G) \/ (the_Edges_of G) by XBOOLE_0:def 3;
<*v'*> 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

thus not len W is even by FINSEQ_1:57, JORDAN12:3; :: 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:57;
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 )
assume n < len <*v*> ; :: thesis: W . (n + 1) Joins W . n,W . (n + 2),G
then ( 1 <= n & n < 1 ) by FINSEQ_1:57, HEYTING3:1;
hence W . (n + 1) Joins W . n,W . (n + 2),G ; :: thesis: verum

end;

hence <*v*> is Walk of G by Def3; :: thesis: verum