let G be _Graph; :: thesis: for W1, W2 being Walk of G st W2 is_odd_substring_of W1, 0 holds
( W1 . (W1 .findFirstVertex W2) = W2 .first() & W1 . (W1 .findLastVertex W2) = W2 .last() )
let W1, W2 be Walk of G; :: thesis: ( W2 is_odd_substring_of W1, 0 implies ( W1 . (W1 .findFirstVertex W2) = W2 .first() & W1 . (W1 .findLastVertex W2) = W2 .last() ) )
assume A1: W2 is_odd_substring_of W1, 0 ; :: thesis: ( W1 . (W1 .findFirstVertex W2) = W2 .first() & W1 . (W1 .findLastVertex W2) = W2 .last() )
then consider k1 being even Nat such that
A2: W1 .findFirstVertex W2 = k1 + 1 and
A3: for n being Nat st 1 <= n & n <= len W2 holds
W1 . (k1 + n) = W2 . n and
for l being even Nat st ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (l + n) = W2 . n ) holds
k1 <= l by Def3;
consider k2 being even Nat such that
A4: W1 .findLastVertex W2 = k2 + (len W2) and
A5: for n being Nat st 1 <= n & n <= len W2 holds
W1 . (k2 + n) = W2 . n and
for l being even Nat st ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (l + n) = W2 . n ) holds
k2 <= l by A1, Def4;
A6: 1 <= len W2 by ABIAN:12;
then W1 . (W1 .findFirstVertex W2) = W2 . 1 by A2, A3;
hence W1 . (W1 .findFirstVertex W2) = W2 .first() by GLIB_001:def 6; :: thesis: W1 . (W1 .findLastVertex W2) = W2 .last()
W1 . (W1 .findLastVertex W2) = W2 . (len W2) by A4, A5, A6;
hence W1 . (W1 .findLastVertex W2) = W2 .last() by GLIB_001:def 7; :: thesis: verum