let G be _Graph; :: thesis: for W being Walk of G

for m being odd Element of NAT st m <= len W holds

len (W .cut (1,m)) = m

let W be Walk of G; :: thesis: for m being odd Element of NAT st m <= len W holds

len (W .cut (1,m)) = m

let m be odd Element of NAT ; :: thesis: ( m <= len W implies len (W .cut (1,m)) = m )

A1: 1 <= m by ABIAN:12;

assume m <= len W ; :: thesis: len (W .cut (1,m)) = m

then (len (W .cut (1,m))) + 1 = m + 1 by A1, Lm15, JORDAN12:2;

hence len (W .cut (1,m)) = m ; :: thesis: verum

for m being odd Element of NAT st m <= len W holds

len (W .cut (1,m)) = m

let W be Walk of G; :: thesis: for m being odd Element of NAT st m <= len W holds

len (W .cut (1,m)) = m

let m be odd Element of NAT ; :: thesis: ( m <= len W implies len (W .cut (1,m)) = m )

A1: 1 <= m by ABIAN:12;

assume m <= len W ; :: thesis: len (W .cut (1,m)) = m

then (len (W .cut (1,m))) + 1 = m + 1 by A1, Lm15, JORDAN12:2;

hence len (W .cut (1,m)) = m ; :: thesis: verum