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:40;

hence G .walkOf v is closed ; :: thesis: ( G .walkOf v is directed & 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:39;

then 0 + 1 = (2 * (len ((G .walkOf v) .edgeSeq()))) + 1 by Def15;

then (G .walkOf v) .length() = 0 ;

hence G .walkOf v is trivial ; :: 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:40;

then (G .walkOf v) .edgeSeq() = {} ;

hence A1: G .walkOf v is Trail-like ; :: thesis: G .walkOf v is Path-like

( 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:40;

hence G .walkOf v is closed ; :: thesis: ( G .walkOf v is directed & G .walkOf v is trivial & G .walkOf v is Trail-like & G .walkOf v is Path-like )

now :: thesis: for n being odd Element of NAT st n < len (G .walkOf v) holds

(G .walkOf v) . n = (the_Source_of G) . ((G .walkOf v) . (n + 1))

hence
G .walkOf v is directed
; :: thesis: ( G .walkOf v is trivial & G .walkOf v is Trail-like & G .walkOf v is Path-like )(G .walkOf v) . n = (the_Source_of G) . ((G .walkOf v) . (n + 1))

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:39;

hence (G .walkOf v) . n = (the_Source_of G) . ((G .walkOf v) . (n + 1)) by ABIAN:12; :: thesis: verum

end;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:39;

hence (G .walkOf v) . n = (the_Source_of G) . ((G .walkOf v) . (n + 1)) by ABIAN:12; :: thesis: verum

len (G .walkOf v) = 1 by FINSEQ_1:39;

then 0 + 1 = (2 * (len ((G .walkOf v) .edgeSeq()))) + 1 by Def15;

then (G .walkOf v) .length() = 0 ;

hence G .walkOf v is trivial ; :: 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:40;

then (G .walkOf v) .edgeSeq() = {} ;

hence A1: G .walkOf v is Trail-like ; :: thesis: G .walkOf v is Path-like

now :: thesis: for n, m being odd Element of NAT st n < m & m <= len (G .walkOf v) & (G .walkOf v) . n = (G .walkOf v) . m holds

( n = 1 & m = len (G .walkOf v) )

hence
G .walkOf v is Path-like
by A1; :: thesis: verum( n = 1 & m = len (G .walkOf v) )

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 that

A2: n < m and

A3: m <= len (G .walkOf v) ; :: thesis: ( (G .walkOf v) . n = (G .walkOf v) . m implies ( n = 1 & m = len (G .walkOf v) ) )

m <= 1 by A3, FINSEQ_1:40;

then n < 1 by A2, XXREAL_0:2;

hence ( (G .walkOf v) . n = (G .walkOf v) . m implies ( n = 1 & m = len (G .walkOf v) ) ) by ABIAN:12; :: thesis: verum

end;assume that

A2: n < m and

A3: m <= len (G .walkOf v) ; :: thesis: ( (G .walkOf v) . n = (G .walkOf v) . m implies ( n = 1 & m = len (G .walkOf v) ) )

m <= 1 by A3, FINSEQ_1:40;

then n < 1 by A2, XXREAL_0:2;

hence ( (G .walkOf v) . n = (G .walkOf v) . m implies ( n = 1 & m = len (G .walkOf v) ) ) by ABIAN:12; :: thesis: verum