let G be _Graph; :: thesis: for v being Vertex of G holds
( G .walkOf v is closed & G .walkOf v is directed & G .walkOf v is trivial & G .walkOf v is Trail-like & G .walkOf v is Path-like )
let v be Vertex of G; :: thesis: ( G .walkOf v is closed & G .walkOf v is directed & G .walkOf v is trivial & G .walkOf v is Trail-like & G .walkOf v is Path-like )
set W = G .walkOf v;
(G .walkOf v) .first() = (G .walkOf v) .last() by FINSEQ_1:57;
hence G .walkOf v is closed by Def24; :: thesis: ( G .walkOf v is directed & G .walkOf v is trivial & G .walkOf v is Trail-like & G .walkOf v is Path-like )

now

let n be odd Element of NAT ; :: thesis: ( n < len (G .walkOf v) implies (G .walkOf v) . n = (the_Source_of G) . ((G .walkOf v) . (n + 1)) )
assume n < len (G .walkOf v) ; :: thesis: (G .walkOf v) . n = (the_Source_of G) . ((G .walkOf v) . (n + 1))
then n < 1 by FINSEQ_1:56;
hence (G .walkOf v) . n = (the_Source_of G) . ((G .walkOf v) . (n + 1)) by HEYTING3:1; :: thesis: verum

end;

hence G .walkOf v is directed by Def25; :: thesis: ( G .walkOf v is trivial & G .walkOf v is Trail-like & G .walkOf v is Path-like )
len (G .walkOf v) = 1 by FINSEQ_1:56;
then 0 + 1 = (2 * (len ((G .walkOf v) .edgeSeq() ))) + 1 by Def15;
then (G .walkOf v) .length() = 0 ;
hence G .walkOf v is trivial by Def26; :: thesis: ( G .walkOf v is Trail-like & G .walkOf v is Path-like )
len (G .walkOf v) = (2 * (len ((G .walkOf v) .edgeSeq() ))) + 1 by Def15;
then 0 + 1 = (2 * (len ((G .walkOf v) .edgeSeq() ))) + 1 by FINSEQ_1:57;
then (G .walkOf v) .edgeSeq() = {} ;
then (G .walkOf v) .edgeSeq() is one-to-one ;
hence A1: G .walkOf v is Trail-like by Def27; :: thesis: G .walkOf v is Path-like

now

let n, m be odd Element of NAT ; :: thesis: ( n < m & m <= len (G .walkOf v) & (G .walkOf v) . n = (G .walkOf v) . m implies ( n = 1 & m = len (G .walkOf v) ) )
assume ( n < m & m <= len (G .walkOf v) ) ; :: thesis: ( (G .walkOf v) . n = (G .walkOf v) . m implies ( n = 1 & m = len (G .walkOf v) ) )
then ( n < m & m <= 1 ) by FINSEQ_1:57;
then n < 1 by XXREAL_0:2;
hence ( (G .walkOf v) . n = (G .walkOf v) . m implies ( n = 1 & m = len (G .walkOf v) ) ) by HEYTING3:1; :: thesis: verum

end;

hence G .walkOf v is Path-like by A1, Def28; :: thesis: verum