let G be _Graph; :: thesis: for W being Walk of G
for n being odd Element of NAT st n <= len W holds
W .vertexAt n = (W .vertexSeq() ) . ((n + 1) div 2)
let W be Walk of G; :: thesis: for n being odd Element of NAT st n <= len W holds
W .vertexAt n = (W .vertexSeq() ) . ((n + 1) div 2)
let n be odd Element of NAT ; :: thesis: ( n <= len W implies W .vertexAt n = (W .vertexSeq() ) . ((n + 1) div 2) )
assume A1: n <= len W ; :: thesis: W .vertexAt n = (W .vertexSeq() ) . ((n + 1) div 2)
then A2: W .vertexAt n = W . n by Def8;
set m = (n + 1) div 2;
( (2 * ((n + 1) div 2)) - 1 = n & 1 <= (n + 1) div 2 & (n + 1) div 2 <= len (W .vertexSeq() ) ) by A1, Th69;
hence W .vertexAt n = (W .vertexSeq() ) . ((n + 1) div 2) by A2, Def14; :: thesis: verum