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

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