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))) + n = (len W) + m

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))) + n = (len W) + m

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

set W1 = W .cut (1,m);

set W2 = W .cut (n,(len W));

assume that

A1: m <= n and

A2: n <= len W and

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

A4: W .remove (m,n) = (W .cut (1,m)) .append (W .cut (n,(len W))) by A1, A2, A3, Def12;

A5: (len (W .cut (n,(len W)))) + n = (len W) + 1 by A2, Lm15;

A6: W . n = (W .cut (n,(len W))) .first() by A2, Lm16;

A7: 1 <= m by ABIAN:12;

A8: m <= len W by A1, A2, XXREAL_0:2;

then A9: (len (W .cut (1,m))) + 1 = m + 1 by A7, Lm15, JORDAN12:2;

(W .cut (1,m)) .last() = W . n by A3, A7, A8, Lm16, JORDAN12:2;

then (len ((W .cut (1,m)) .append (W .cut (n,(len W))))) + 1 = m + (((len W) + 1) + (- n)) by A6, A9, A5, Lm9

.= (((len W) + m) + (- n)) + 1 ;

hence (len (W .remove (m,n))) + n = (len W) + m by A4; :: 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))) + n = (len W) + m

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))) + n = (len W) + m

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

set W1 = W .cut (1,m);

set W2 = W .cut (n,(len W));

assume that

A1: m <= n and

A2: n <= len W and

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

A4: W .remove (m,n) = (W .cut (1,m)) .append (W .cut (n,(len W))) by A1, A2, A3, Def12;

A5: (len (W .cut (n,(len W)))) + n = (len W) + 1 by A2, Lm15;

A6: W . n = (W .cut (n,(len W))) .first() by A2, Lm16;

A7: 1 <= m by ABIAN:12;

A8: m <= len W by A1, A2, XXREAL_0:2;

then A9: (len (W .cut (1,m))) + 1 = m + 1 by A7, Lm15, JORDAN12:2;

(W .cut (1,m)) .last() = W . n by A3, A7, A8, Lm16, JORDAN12:2;

then (len ((W .cut (1,m)) .append (W .cut (n,(len W))))) + 1 = m + (((len W) + 1) + (- n)) by A6, A9, A5, Lm9

.= (((len W) + m) + (- n)) + 1 ;

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