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

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

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

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

hence
W .remove (m,n) is Subwalk of W
; :: 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 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;

A5: 2 divides lenWaa1 by PEPIN:22;

then A6: lenWaa1 = 2 * (lenWaa1 div 2) by NAT_D: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 A19: { x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } c= Seg (len (W .edgeSeq())) by XBOOLE_1:11;

A20: { x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } c= Seg (len (W .edgeSeq())) by A18, XBOOLE_1:11;

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

A22: (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;

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 14;

set lenY = (lenWaa1 div 2) - n1div2aa1;

A30: Y = { x where x is Nat : ( n1div2aa1 + 1 <= x & x <= n1div2aa1 + lenY ) } ;

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;

then A52: card Z = (maa1 div 2) + (lenWn4 div 2) by A40, A25, CARD_2:40;

dom es c= Seg (len (W .edgeSeq())) by A22, A18, RELAT_1:61;

then rng (Sgm (dom es)) = dom es by FINSEQ_1:def 13;

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 A18, A25, FINSEQ_3:40, XBOOLE_1:11;

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

then reconsider n1div2aa1 = (n1 div 2) - 1 as Element of NAT by INT_1:5;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 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

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())

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

end;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())end;

hence
x in dom (W .edgeSeq())
; :: thesis: verumper 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;

end;

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

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

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 A19: { x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } c= Seg (len (W .edgeSeq())) by XBOOLE_1:11;

A20: { x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } c= Seg (len (W .edgeSeq())) by A18, XBOOLE_1:11;

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

A22: (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 2end;

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;per cases
( n1 div 2 > lenWaa1 div 2 or n1 div 2 <= lenWaa1 div 2 )
;

end;

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;

end;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 <> {}

hence
card Y = lenWn4 div 2
by A27, NAT_2:2; :: thesis: verumassume
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;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

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

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 14;

set lenY = (lenWaa1 div 2) - n1div2aa1;

now :: thesis: not n1div2aa1 > lenWaa1 div 2

then reconsider lenY = (lenWaa1 div 2) - n1div2aa1 as Element of NAT by INT_1:5;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 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

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

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

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

then A44:
dom (Sgm X) = Seg (maa1 div 2)
by A18, FINSEQ_3:40, XBOOLE_1:11;per cases
( maa1 div 2 = 0 or maa1 div 2 <> 0 )
;

end;

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

end;

now :: thesis: not X <> {}

hence
card X = maa1 div 2
by A41; :: thesis: verumassume
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;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

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 = {}

then
X misses Y
by XBOOLE_0:def 7;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 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

then A52: card Z = (maa1 div 2) + (lenWn4 div 2) by A40, A25, CARD_2:40;

dom es c= Seg (len (W .edgeSeq())) by A22, A18, RELAT_1:61;

then rng (Sgm (dom es)) = dom es by FINSEQ_1:def 13;

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 A18, A25, FINSEQ_3:40, XBOOLE_1:11;

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

then A81:
(W .remove (m,n)) .edgeSeq() = Seq es
by A3, A24, A2, A53, A46, A52, FUNCT_1:2;((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;

end;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) . x9end;

hence
((W .remove (m,n)) .edgeSeq()) . x9 = (Seq es) . x9
; :: thesis: verumper cases
( (2 * x) + 1 <= m or (2 * x) + 1 > m )
;

end;

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;((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

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

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;

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;

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;

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

then consider k being Nat such that 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 2 * x <= maa1 by A3, XREAL_1:64;

then (2 * x) + 1 <= maa1 + 1 by XREAL_1:7;

hence contradiction by A66; :: thesis: verum

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

k <> 0
by A67, A68;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;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

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)

then
k in dom (Sgm Y)
by A54, A68, A76, FINSEQ_1:1;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;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

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

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