let G be _Graph; :: thesis: for W being Walk of G
for n being odd Element of NAT st n <= len W holds
W .cut n,n = <*(W .vertexAt n)*>
let W be Walk of G; :: thesis: for n being odd Element of NAT st n <= len W holds
W .cut n,n = <*(W .vertexAt n)*>
let n be odd Element of NAT ; :: thesis: ( n <= len W implies W .cut n,n = <*(W .vertexAt n)*> )
A1: 1 <= n by HEYTING3:1;
assume A2: n <= len W ; :: thesis: W .cut n,n = <*(W .vertexAt n)*>
then A3: W . n = W .vertexAt n by Def8;
W .cut n,n = n,n -cut W by A2, Def11;
hence W .cut n,n = <*(W .vertexAt n)*> by A2, A3, A1, GRAPH_2:6; :: thesis: verum