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

for m, n being Element of NAT

for x, y being set st W is_Walk_from x,y holds

W .remove (m,n) is_Walk_from x,y

let W be Walk of G; :: thesis: for m, n being Element of NAT

for x, y being set st W is_Walk_from x,y holds

W .remove (m,n) is_Walk_from x,y

let m, n be Element of NAT ; :: thesis: for x, y being set st W is_Walk_from x,y holds

W .remove (m,n) is_Walk_from x,y

let x, y be set ; :: thesis: ( W is_Walk_from x,y implies W .remove (m,n) is_Walk_from x,y )

set W2 = W .remove (m,n);

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

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

assume A1: W is_Walk_from x,y ; :: thesis: W .remove (m,n) is_Walk_from x,y

for m, n being Element of NAT

for x, y being set st W is_Walk_from x,y holds

W .remove (m,n) is_Walk_from x,y

let W be Walk of G; :: thesis: for m, n being Element of NAT

for x, y being set st W is_Walk_from x,y holds

W .remove (m,n) is_Walk_from x,y

let m, n be Element of NAT ; :: thesis: for x, y being set st W is_Walk_from x,y holds

W .remove (m,n) is_Walk_from x,y

let x, y be set ; :: thesis: ( W is_Walk_from x,y implies W .remove (m,n) is_Walk_from x,y )

set W2 = W .remove (m,n);

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

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

assume A1: W is_Walk_from x,y ; :: thesis: W .remove (m,n) is_Walk_from x,y

now :: thesis: W .remove (m,n) is_Walk_from x,yend;

hence
W .remove (m,n) is_Walk_from x,y
; :: thesis: verumper cases
( ( m is odd & n is odd & m <= n & n <= len W & W . m = W . n ) or not m is odd or not n is odd or not m <= n or not n <= len W or not W . m = W . n )
;

end;

suppose A2:
( m is odd & n is odd & m <= n & n <= len W & W . m = W . n )
; :: thesis: W .remove (m,n) is_Walk_from x,y

then A3: (W .cut (n,(len W))) .last() =
W .last()
by Lm16

.= y by A1 ;

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

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

A6: 1 <= m by A2, ABIAN:12;

then A7: (W .cut (1,m)) .first() = W .first() by A2, A5, Lm16, JORDAN12:2

.= x by A1 ;

(W .cut (1,m)) .last() = W . n by A2, A6, A5, Lm16, JORDAN12:2

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

hence W .remove (m,n) is_Walk_from x,y by A4, A7, A3, Lm11; :: thesis: verum

end;.= y by A1 ;

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

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

A6: 1 <= m by A2, ABIAN:12;

then A7: (W .cut (1,m)) .first() = W .first() by A2, A5, Lm16, JORDAN12:2

.= x by A1 ;

(W .cut (1,m)) .last() = W . n by A2, A6, A5, Lm16, JORDAN12:2

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

hence W .remove (m,n) is_Walk_from x,y by A4, A7, A3, Lm11; :: thesis: verum

suppose
( not m is odd or not n is odd or not m <= n or not n <= len W or not W . m = W . n )
; :: thesis: W .remove (m,n) is_Walk_from x,y

end;

end;