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

now :: thesis: W .remove (m,n) is Subwalk of W

per 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 ) ;

suppose A1: ( m is odd & n is odd & m <= n & n <= len W & W . m = W . n ) ; :: thesis: W .remove (m,n) is Subwalk of W

then reconsider m9 = m, n9 = n as odd Element of NAT ;
reconsider lenWn4 = (len W) - n9 as even Element of NAT by A1, INT_1:5;
A2: Seg (len ((W .remove (m,n)) .edgeSeq())) = dom ((W .remove (m,n)) .edgeSeq()) by FINSEQ_1:def 3;
reconsider lenWaa1 = (len W) - 1 as even Element of NAT by ABIAN:12, INT_1:5;
reconsider n1 = n9 + 1 as even Element of NAT ;
reconsider maa1 = m9 - 1 as even Element of NAT by ABIAN:12, INT_1:5;
set X = { x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } ;
set Y = { x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } ;
set Z = { x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } \/ { x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } ;
set es = (W .edgeSeq()) | ( { x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } \/ { x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } );
2 divides maa1 by PEPIN:22;
then A3: maa1 = 2 * (maa1 div 2) by NAT_D:3;
2 divides n1 by PEPIN:22;
then A4: n1 = 2 * (n1 div 2) by NAT_D:3;

now :: thesis: not n1 div 2 < 1

assume n1 div 2 < 1 ; :: thesis: contradiction
then 2 * (n1 div 2) < 2 * 1 by XREAL_1:68;
then (n + 1) - 1 < 2 - 1 by A4, XREAL_1:14;
then n9 < 1 ;
hence contradiction by ABIAN:12; :: thesis: verum

end;

then reconsider n1div2aa1 = (n1 div 2) - 1 as Element of NAT by INT_1:5;
A5: 2 divides lenWaa1 by PEPIN:22;
then A6: lenWaa1 = 2 * (lenWaa1 div 2) by NAT_D:3;

now :: thesis: for x being object st x in { x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } \/ { x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } holds
x in dom (W .edgeSeq())

let x be object ; :: thesis: ( x in { x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } \/ { x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } implies x in dom (W .edgeSeq()) )
assume A7: x in { x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } \/ { x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } ; :: thesis: x in dom (W .edgeSeq())

now :: thesis: x in dom (W .edgeSeq())

per cases ( x in { x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } or x in { x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } ) by A7, XBOOLE_0:def 3;

suppose x in { x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } ; :: thesis: x in dom (W .edgeSeq())

then consider y being Nat such that
A8: y = x and
A9: 1 <= y and
A10: y <= maa1 div 2 ;
2 * y <= maa1 by A3, A10, XREAL_1:64;
then 2 * y <= maa1 + 1 by NAT_1:12;
then 2 * y <= n by A1, XXREAL_0:2;
then A11: 2 * y <= len W by A1, XXREAL_0:2;
1 <= y + y by A9, NAT_1:12;
then 2 * y in dom W by A11, FINSEQ_3:25;
hence x in dom (W .edgeSeq()) by A8, Lm41; :: thesis: verum

end;

suppose x in { x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } ; :: thesis: x in dom (W .edgeSeq())

then consider y being Nat such that
A12: y = x and
A13: n1 div 2 <= y and
A14: y <= lenWaa1 div 2 ;
2 * y <= lenWaa1 by A6, A14, XREAL_1:64;
then A15: 2 * y <= lenWaa1 + 1 by NAT_1:12;
A16: 1 <= n1 by NAT_1:12;
n1 <= 2 * y by A4, A13, XREAL_1:64;
then 1 <= 2 * y by A16, XXREAL_0:2;
then 2 * y in dom W by A15, FINSEQ_3:25;
hence x in dom (W .edgeSeq()) by A12, Lm41; :: thesis: verum

end;

end;

end;

hence x in dom (W .edgeSeq()) ; :: thesis: verum

end;

then A17: { x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } \/ { x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } c= dom (W .edgeSeq()) by TARSKI:def 3;
then A18: { x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } \/ { x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } c= Seg (len (W .edgeSeq())) by FINSEQ_1:def 3;
then a18: { x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } \/ { x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } is included_in_Seg by FINSEQ_1:def 13;
{ x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } c= Seg (len (W .edgeSeq())) by A18, XBOOLE_1:11;
then a19: { x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } is included_in_Seg by FINSEQ_1:def 13;
{ x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } c= Seg (len (W .edgeSeq())) by A18, XBOOLE_1:11;
then a20: { x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } is included_in_Seg by FINSEQ_1:def 13;
reconsider X = { x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } , Y = { x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } as finite set by A18, FINSET_1:1, XBOOLE_1:11;
A21: X = { x where x is Nat : ( 0 + 1 <= x & x <= 0 + (maa1 div 2) ) } ;
(dom (W .edgeSeq())) /\ ( { x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } \/ { x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } ) = { x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } \/ { x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } by A17, XBOOLE_1:28;
then A23: dom ((W .edgeSeq()) | ( { x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } \/ { x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } )) = { x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } \/ { x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } by RELAT_1:61;
2 divides lenWn4 by PEPIN:22;
then A24: lenWn4 = 2 * (lenWn4 div 2) by NAT_D:3;

A25: now :: thesis: card Y = lenWn4 div 2

per cases ( n1 div 2 > lenWaa1 div 2 or n1 div 2 <= lenWaa1 div 2 ) ;

suppose A26: n1 div 2 > lenWaa1 div 2 ; :: thesis: card Y = lenWn4 div 2

then lenWaa1 < n + 1 by A6, A4, XREAL_1:68;
then lenWaa1 + 1 <= n + 1 by NAT_1:13;
then len W <= n9 + 1 ;
then len W < n + 1 by XXREAL_0:1;
then len W <= n by NAT_1:13;
then A27: len W = n by A1, XXREAL_0:1;

now :: thesis: not Y <> {}

assume Y <> {} ; :: thesis: contradiction
then consider x being object such that
A28: x in Y by XBOOLE_0:def 1;
ex x9 being Nat st
( x9 = x & n1 div 2 <= x9 & x9 <= lenWaa1 div 2 ) by A28;
hence contradiction by A26, XXREAL_0:2; :: thesis: verum

end;

hence card Y = lenWn4 div 2 by A27; :: thesis: verum

end;

suppose n1 div 2 <= lenWaa1 div 2 ; :: thesis: card Y = lenWn4 div 2

then reconsider k = (lenWaa1 div 2) - (n1 div 2) as Element of NAT by INT_1:5;
Y = { x where x is Nat : ( n1 div 2 <= x & x <= (n1 div 2) + k ) } ;
then card Y = k + 1 by FINSEQ_6:130;
hence card Y = lenWn4 div 2 by A24, A6, A4; :: thesis: verum

end;

end;

end;

reconsider Z = { x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } \/ { x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } as finite set by A17;
W .edgeSeq() is Subset of (W .edgeSeq()) by FINSEQ_6:152;
then reconsider es = (W .edgeSeq()) | ( { x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } \/ { x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } ) as Subset of (W .edgeSeq()) by FINSEQ_6:153;
set es2 = Seq es;
A29: Seq es = es * (Sgm (dom es)) by FINSEQ_1:def 15;
set lenY = (lenWaa1 div 2) - n1div2aa1;

now :: thesis: not n1div2aa1 > lenWaa1 div 2

assume n1div2aa1 > lenWaa1 div 2 ; :: thesis: contradiction
then 2 * n1div2aa1 > 2 * (lenWaa1 div 2) by XREAL_1:68;
then ((n + 1) - 1) - 1 > (len W) - 1 by A5, A4, NAT_D:3;
hence contradiction by A1, XREAL_1:9; :: thesis: verum

end;

then reconsider lenY = (lenWaa1 div 2) - n1div2aa1 as Element of NAT by INT_1:5;
A30: Y = { x where x is Nat : ( n1div2aa1 + 1 <= x & x <= n1div2aa1 + lenY ) } ;

A31: now :: thesis: for a, b being Nat st a in X & b in Y holds
a < b

let a, b be Nat; :: thesis: ( a in X & b in Y implies a < b )
assume that
A32: a in X and
A33: b in Y ; :: thesis: a < b
consider b9 being Nat such that
A34: b9 = b and
A35: n1 div 2 <= b9 and
b9 <= lenWaa1 div 2 by A33;
consider a9 being Nat such that
A36: a9 = a and
1 <= a9 and
A37: a9 <= maa1 div 2 by A32;
2 * a9 <= maa1 by A3, A37, XREAL_1:64;
then 2 * a9 < maa1 + 1 by NAT_1:13;
then 2 * a9 < n by A1, XXREAL_0:2;
then A38: (2 * a9) + 0 < n + 1 by XREAL_1:8;
A39: n + 1 <= 2 * b9 by A4, A35, XREAL_1:64;
then 2 * a9 < 2 * b9 by A38, XXREAL_0:2;
then a9 <= b9 by XREAL_1:68;
hence a < b by A36, A34, A38, A39, XXREAL_0:1; :: thesis: verum

end;

A40: now :: thesis: card X = maa1 div 2

per cases ( maa1 div 2 = 0 or maa1 div 2 <> 0 ) ;

suppose A41: maa1 div 2 = 0 ; :: thesis: card X = maa1 div 2

now :: thesis: not X <> {}

assume X <> {} ; :: thesis: contradiction
then consider x being object such that
A42: x in X by XBOOLE_0:def 1;
ex x9 being Nat st
( x9 = x & 1 <= x9 & x9 <= maa1 div 2 ) by A42;
hence contradiction by A41; :: thesis: verum

end;

hence card X = maa1 div 2 by A41; :: thesis: verum

end;

suppose maa1 div 2 <> 0 ; :: thesis: card X = maa1 div 2

then consider k being Nat such that
A43: maa1 div 2 = k + 1 by NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
maa1 div 2 = k + 1 by A43;
hence card X = maa1 div 2 by FINSEQ_6:130; :: thesis: verum

end;

end;

end;

then A44: dom (Sgm X) = Seg (maa1 div 2) by a19, FINSEQ_3:40;
then A45: len (Sgm X) = maa1 div 2 by FINSEQ_1:def 3;
len (W .remove (m,n)) = (2 * (len ((W .remove (m,n)) .edgeSeq()))) + 1 by Def15;
then A46: ((len W) + m) - n = (2 * (len ((W .remove (m,n)) .edgeSeq()))) + 1 by A1, Lm31;

now :: thesis: X /\ Y = {}

assume not X /\ Y = {} ; :: thesis: contradiction
then consider x being object such that
A47: x in X /\ Y by XBOOLE_0:def 1;
x in Y by A47, XBOOLE_0:def 4;
then consider y9 being Nat such that
A48: y9 = x and
A49: n1 div 2 <= y9 and
y9 <= lenWaa1 div 2 ;
x in X by A47, XBOOLE_0:def 4;
then consider x9 being Nat such that
A50: x9 = x and
1 <= x9 and
A51: x9 <= maa1 div 2 ;
2 * x9 <= maa1 by A3, A51, XREAL_1:64;
then 2 * y9 < maa1 + 1 by A50, A48, NAT_1:13;
then 2 * y9 < n by A1, XXREAL_0:2;
then (2 * y9) + 0 < n + 1 by XREAL_1:8;
hence contradiction by A4, A49, XREAL_1:64; :: thesis: verum

end;

then X misses Y by XBOOLE_0:def 7;
then A52: card Z = (maa1 div 2) + (lenWn4 div 2) by A40, A25, CARD_2:40;
rng (Sgm (dom es)) = dom es by FINSEQ_1:def 14;
then A53: dom (Seq es) = dom (Sgm Z) by A23, A29, RELAT_1:27
.= Seg (card Z) by a18, FINSEQ_3:40 ;
A54: dom (Sgm Y) = Seg (lenWn4 div 2) by a20, A25, FINSEQ_3:40;

now :: thesis: for x9 being object st x9 in dom ((W .remove (m,n)) .edgeSeq()) holds
((W .remove (m,n)) .edgeSeq()) . x9 = (Seq es) . x9

let x9 be object ; :: thesis: ( x9 in dom ((W .remove (m,n)) .edgeSeq()) implies ((W .remove (m,n)) .edgeSeq()) . x9 = (Seq es) . x9 )
assume A55: x9 in dom ((W .remove (m,n)) .edgeSeq()) ; :: thesis: ((W .remove (m,n)) .edgeSeq()) . x9 = (Seq es) . x9
then reconsider x = x9 as Element of NAT ;
A56: 1 <= x by A55, FINSEQ_3:25;
A57: x <= len ((W .remove (m,n)) .edgeSeq()) by A55, FINSEQ_3:25;
then A58: ((W .remove (m,n)) .edgeSeq()) . x = (W .remove (m,n)) . (2 * x) by A56, Def15;

now :: thesis: ((W .remove (m,n)) .edgeSeq()) . x9 = (Seq es) . x9

per cases ( (2 * x) + 1 <= m or (2 * x) + 1 > m ) ;

suppose A59: (2 * x) + 1 <= m ; :: thesis: ((W .remove (m,n)) .edgeSeq()) . x9 = (Seq es) . x9

A60: 1 <= x + x by A56, NAT_1:12;
((2 * x) + 1) - 1 < m - 0 by A59, XREAL_1:15;
then 2 * x in Seg m by A60, FINSEQ_1:1;
then A61: ((W .remove (m,n)) .edgeSeq()) . x9 = W . (2 * x) by A1, A58, Lm29;
A62: (Sgm Z) . x = ((Sgm X) ^ (Sgm Y)) . x by a19, a20, A31, FINSEQ_3:42;
((2 * x) + 1) - 1 <= maa1 by A59, XREAL_1:13;
then A63: x <= maa1 div 2 by A3, XREAL_1:68;
then x in X by A56;
then A64: x in dom es by A23, XBOOLE_0:def 3;
x in dom (Sgm X) by A44, A56, A63, FINSEQ_1:1;
then (Sgm Z) . x = (Sgm X) . x by A62, FINSEQ_1:def 7
.= 0 + x by A21, A56, A63, FINSEQ_6:131 ;
then (Seq es) . x = es . x by A3, A24, A23, A2, A29, A53, A46, A52, A55, FUNCT_1:12;
then A65: (Seq es) . x = (W .edgeSeq()) . x by A64, FUNCT_1:47;
x <= len (W .edgeSeq()) by A23, A18, A64, FINSEQ_1:1;
hence ((W .remove (m,n)) .edgeSeq()) . x9 = (Seq es) . x9 by A56, A61, A65, Def15; :: thesis: verum

end;

suppose A66: (2 * x) + 1 > m ; :: thesis: ((W .remove (m,n)) .edgeSeq()) . x9 = (Seq es) . x9

A67: now :: thesis: not x <= maa1 div 2

assume x <= maa1 div 2 ; :: thesis: contradiction
then 2 * x <= maa1 by A3, XREAL_1:64;
then (2 * x) + 1 <= maa1 + 1 by XREAL_1:7;
hence contradiction by A66; :: thesis: verum

end;

then consider k being Nat such that
A68: x = (maa1 div 2) + k by NAT_1:10;
A69: (Sgm Z) . x = ((Sgm X) ^ (Sgm Y)) . x by a19, a20, A31, FINSEQ_3:42;
A70: ex lenWaa19 being even Element of NAT st
( lenWaa19 = lenWaa1 & len (W .edgeSeq()) = lenWaa19 div 2 ) by Lm42;
2 * x <= 2 * (len ((W .remove (m,n)) .edgeSeq())) by A57, XREAL_1:64;
then 2 * x <= (2 * (len ((W .remove (m,n)) .edgeSeq()))) + 1 by NAT_1:12;
then A71: 2 * x <= len (W .remove (m,n)) by Def15;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
A72: 2 * (n1div2aa1 + k) = ((2 * x) - m) + n by A3, A4, A68;
A73: m <= 2 * x by A66, NAT_1:13;
then A74: ((2 * x) - m) + n <= len W by A1, A71, Lm30;

A75: now :: thesis: not lenWaa1 div 2 < k + n1div2aa1

reconsider z = ((2 * x) - m9) + n9 as Element of NAT by A1, A73, A71, Lm30;
assume lenWaa1 div 2 < k + n1div2aa1 ; :: thesis: contradiction
then lenWaa1 < 2 * ((x - (maa1 div 2)) + n1div2aa1) by A6, A68, XREAL_1:68;
then lenWaa1 + 1 < (((2 * x) - m) + n) + 1 by A3, A4, XREAL_1:8;
then len W <= z by NAT_1:13;
hence contradiction by A74, XXREAL_0:1; :: thesis: verum

end;

k <> 0 by A67, A68;
then 0 + 1 < k + 1 by XREAL_1:8;
then A76: 1 <= k by NAT_1:13;
then n1div2aa1 + 1 <= n1div2aa1 + k by XREAL_1:7;
then n1div2aa1 + k in Y by A75;
then n1div2aa1 + k in dom es by A23, XBOOLE_0:def 3;
then A77: es . (n1div2aa1 + k) = (W .edgeSeq()) . (n1div2aa1 + k) by FUNCT_1:47;

A78: now :: thesis: not lenWn4 div 2 < x - (maa1 div 2)

set z = ((2 * x) - m9) + n9;
reconsider z = ((2 * x) - m9) + n9 as Element of NAT by A1, A73, A71, Lm30;
assume lenWn4 div 2 < x - (maa1 div 2) ; :: thesis: contradiction
then 2 * (lenWn4 div 2) < 2 * (x - (maa1 div 2)) by XREAL_1:68;
then A79: lenWn4 + n < (((2 * x) - m) + 1) + n by A3, A24, XREAL_1:8;
((2 * x) - m9) + n9 < len W by A74, XXREAL_0:1;
then z + 1 <= len W by NAT_1:13;
hence contradiction by A79; :: thesis: verum

end;

then k in dom (Sgm Y) by A54, A68, A76, FINSEQ_1:1;
then (Sgm Z) . x = (Sgm Y) . k by A45, A69, A68, FINSEQ_1:def 7
.= n1div2aa1 + k by A24, A6, A4, A30, A68, A76, A78, FINSEQ_6:131 ;
then A80: (Seq es) . x = es . (n1div2aa1 + k) by A3, A24, A23, A2, A29, A53, A46, A52, A55, FUNCT_1:12;
1 <= n1div2aa1 + k by A76, NAT_1:12;
then (Seq es) . x = W . (2 * (n1div2aa1 + k)) by A80, A75, A77, A70, Def15;
hence ((W .remove (m,n)) .edgeSeq()) . x9 = (Seq es) . x9 by A1, A58, A73, A71, A72, Lm30; :: thesis: verum

end;

end;

end;

hence ((W .remove (m,n)) .edgeSeq()) . x9 = (Seq es) . x9 ; :: thesis: verum

end;

then A81: (W .remove (m,n)) .edgeSeq() = Seq es by A3, A24, A2, A53, A46, A52, FUNCT_1:2;
W is_Walk_from W .first() ,W .last() ;
then W .remove (m,n) is_Walk_from W .first() ,W .last() by Lm25;
hence W .remove (m,n) is Subwalk of W by A81, Def32; :: thesis: verum

end;

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 Subwalk of W

then W .remove (m,n) = W by Def12;
hence W .remove (m,n) is Subwalk of W by Lm70; :: thesis: verum

end;

end;

end;

hence W .remove (m,n) is Subwalk of W ; :: thesis: verum