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 V5() & 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 V5() & 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 V5() & 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))
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;
hence G .walkOf v is directed ; :: thesis: ( G .walkOf v is V5() & G .walkOf v is Trail-like & G .walkOf v is Path-like )
thus G .walkOf v is V5() ; :: 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) )
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;
hence G .walkOf v is Path-like by A1; :: thesis: verum