let G be _Graph; :: thesis: for W being Walk of G
for m being Element of NAT holds W .remove m,m = W
let W be Walk of G; :: thesis: for m being Element of NAT holds W .remove m,m = W
let m be Element of NAT ; :: thesis: W .remove m,m = W

now

per cases ( ( not m is even & m <= len W & W . m = W . m ) or m is even or not m <= len W or not W . m = W . m ) ;

suppose A1: ( not m is even & m <= len W & W . m = W . m ) ; :: thesis: W .remove m,m = W

then A2: 1 <= m by ABIAN:12;
thus W .remove m,m = (W .cut 1,m) .append (W .cut m,(len W)) by A1, Def12
.= W .cut 1,(len W) by A1, A2, Lm17, JORDAN12:3
.= W by Lm18 ; :: thesis: verum

end;

suppose ( m is even or not m <= len W or not W . m = W . m ) ; :: thesis: W .remove m,m = W

hence W .remove m,m = W by Def12; :: thesis: verum

end;

end;

end;

hence W .remove m,m = W ; :: thesis: verum