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 :: thesis: W .remove (m,m) = W

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

suppose A1: ( m is odd & 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:2
.= W by Lm18 ; :: thesis: verum

end;

suppose ( not m is odd 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