let G be _Graph; :: thesis: for W being Walk of G holds
( 1 = W .findFirstVertex W & W .findLastVertex W = len W )
let W be Walk of G; :: thesis: ( 1 = W .findFirstVertex W & W .findLastVertex W = len W )
A2: W is_odd_substring_of W, 0 by Th15, ABIAN:12;
set n1 = W .findFirstVertex W;
set n2 = W .findLastVertex W;
consider k1 being even Nat such that
A3: W .findFirstVertex W = k1 + 1 and
for n being Nat st 1 <= n & n <= len W holds
W . (k1 + n) = W . n and
A5: for l being even Nat st ( for n being Nat st 1 <= n & n <= len W holds
W . (l + n) = W . n ) holds
k1 <= l by A2, Def3;
A6: for n being Nat st 1 <= n & n <= len W holds
W . (0 + n) = W . n ;
then k1 <= 0 by A5;
then k1 = 0 ;
hence 1 = W .findFirstVertex W by A3; :: thesis: W .findLastVertex W = len W
consider k2 being even Nat such that
A7: W .findLastVertex W = k2 + (len W) and
for n being Nat st 1 <= n & n <= len W holds
W . (k2 + n) = W . n and
A9: for l being even Nat st ( for n being Nat st 1 <= n & n <= len W holds
W . (l + n) = W . n ) holds
k2 <= l by A2, Def4;
k2 <= 0 by A6, A9;
then k2 = 0 ;
hence W .findLastVertex W = len W by A7; :: thesis: verum