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

for m, n being odd Element of NAT st m <= n & n <= len W & W . m = W . n holds

len (W .remove (m,n)) = ((len W) + m) - n

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

len (W .remove (m,n)) = ((len W) + m) - n

let m, n be odd Element of NAT ; :: thesis: ( m <= n & n <= len W & W . m = W . n implies len (W .remove (m,n)) = ((len W) + m) - n )

assume that

A1: m <= n and

A2: n <= len W and

A3: W . m = W . n ; :: thesis: len (W .remove (m,n)) = ((len W) + m) - n

(len (W .remove (m,n))) + n = (len W) + m by A1, A2, A3, Lm24;

hence len (W .remove (m,n)) = ((len W) + m) - n ; :: thesis: verum

for m, n being odd Element of NAT st m <= n & n <= len W & W . m = W . n holds

len (W .remove (m,n)) = ((len W) + m) - n

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

len (W .remove (m,n)) = ((len W) + m) - n

let m, n be odd Element of NAT ; :: thesis: ( m <= n & n <= len W & W . m = W . n implies len (W .remove (m,n)) = ((len W) + m) - n )

assume that

A1: m <= n and

A2: n <= len W and

A3: W . m = W . n ; :: thesis: len (W .remove (m,n)) = ((len W) + m) - n

(len (W .remove (m,n))) + n = (len W) + m by A1, A2, A3, Lm24;

hence len (W .remove (m,n)) = ((len W) + m) - n ; :: thesis: verum