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) )

set m = (n + 1) div 2;

assume A1: n <= len W ; :: thesis: W .vertexAt n = (W .vertexSeq()) . ((n + 1) div 2)

then A2: (2 * ((n + 1) div 2)) - 1 = n by Th66;

A3: (n + 1) div 2 <= len (W .vertexSeq()) by A1, Th66;

A4: 1 <= (n + 1) div 2 by A1, Th66;

W .vertexAt n = W . n by A1, Def8;

hence W .vertexAt n = (W .vertexSeq()) . ((n + 1) div 2) by A2, A4, A3, Def14; :: thesis: verum

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) )

set m = (n + 1) div 2;

assume A1: n <= len W ; :: thesis: W .vertexAt n = (W .vertexSeq()) . ((n + 1) div 2)

then A2: (2 * ((n + 1) div 2)) - 1 = n by Th66;

A3: (n + 1) div 2 <= len (W .vertexSeq()) by A1, Th66;

A4: 1 <= (n + 1) div 2 by A1, Th66;

W .vertexAt n = W . n by A1, Def8;

hence W .vertexAt n = (W .vertexSeq()) . ((n + 1) div 2) by A2, A4, A3, Def14; :: thesis: verum