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

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) = Wend;

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

end;