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:3;
hence len (W .cut (1,m)) = m ; :: thesis: verum