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 ABIAN:12;
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, FINSEQ_6:132; :: thesis: verum