let F be FinSequence of INT ; :: thesis: for m, n, ma being Nat st 1 <= m & m <= n & n <= len F holds

( ma = min_at (F,m,n) iff ( m <= ma & ma <= n & ( for i being Nat st m <= i & i <= n holds

F . ma <= F . i ) & ( for i being Nat st m <= i & i < ma holds

F . ma < F . i ) ) )

let m, n, ma be Nat; :: thesis: ( 1 <= m & m <= n & n <= len F implies ( ma = min_at (F,m,n) iff ( m <= ma & ma <= n & ( for i being Nat st m <= i & i <= n holds

F . ma <= F . i ) & ( for i being Nat st m <= i & i < ma holds

F . ma < F . i ) ) ) )

assume that

A1: 1 <= m and

A2: m <= n and

A3: n <= len F ; :: thesis: ( ma = min_at (F,m,n) iff ( m <= ma & ma <= n & ( for i being Nat st m <= i & i <= n holds

F . ma <= F . i ) & ( for i being Nat st m <= i & i < ma holds

F . ma < F . i ) ) )

set Cut = (m,n) -cut F;

A4: (len ((m,n) -cut F)) + m = n + 1 by A1, A2, A3, Def1;

A31: (len ((m,n) -cut F)) + m = n + 1 by A1, A2, A3, Def1;

then A32: len ((m,n) -cut F) = (n + 1) - m ;

set X = rng ((m,n) -cut F);

A33: rng ((m,n) -cut F) is Subset of INT ;

m < n + 1 by A2, NAT_1:13;

then m - m < (n + 1) - m by XREAL_1:9;

then not (m,n) -cut F is empty by A31;

then reconsider X = rng ((m,n) -cut F) as non empty finite Subset of INT by A33;

reconsider rX = X as non empty finite Subset of REAL by MEMBERED:3;

assume that

A34: m <= ma and

A35: ma <= n and

A36: for i being Nat st m <= i & i <= n holds

F . ma <= F . i and

A37: for i being Nat st m <= i & i < ma holds

F . ma < F . i ; :: thesis: ma = min_at (F,m,n)

m - m <= ma - m by A34, XREAL_1:9;

then reconsider qm = ma - m as Element of NAT by INT_1:3;

A38: qm + 1 = (ma + 1) - m ;

then reconsider q1 = (ma + 1) - m as Element of NAT ;

ma + 1 <= n + 1 by A35, XREAL_1:6;

then A39: q1 <= len ((m,n) -cut F) by A32, XREAL_1:9;

0 + 1 <= qm + 1 by XREAL_1:6;

then A40: q1 in dom ((m,n) -cut F) by A39, FINSEQ_3:25;

A41: ma = qm + m ;

qm < len ((m,n) -cut F) by A38, A39, NAT_1:13;

then A42: F . ma = ((m,n) -cut F) . ((ma + 1) - m) by A1, A2, A3, A38, A41, Def1;

set mX = min X;

set mXC = (min X) .. ((m,n) -cut F);

A48: min X in X by XXREAL_2:def 7;

then 1 <= (min X) .. ((m,n) -cut F) by FINSEQ_4:21;

then 1 - 1 <= ((min X) .. ((m,n) -cut F)) - 1 by XREAL_1:9;

then reconsider mXC1 = ((min X) .. ((m,n) -cut F)) - 1 as Element of NAT by INT_1:3;

set mXCm = mXC1 + m;

(min X) .. ((m,n) -cut F) <= len ((m,n) -cut F) by A48, FINSEQ_4:21;

then A49: mXC1 < len ((m,n) -cut F) by XREAL_1:146, XXREAL_0:2;

(min X) .. ((m,n) -cut F) = mXC1 + 1 ;

then A50: F . (mXC1 + m) = ((m,n) -cut F) . ((min X) .. ((m,n) -cut F)) by A1, A2, A3, A49, Def1;

A51: m <= mXC1 + m by NAT_1:12;

A52: ((m,n) -cut F) . ((min X) .. ((m,n) -cut F)) = min X by A48, FINSEQ_4:19;

hence ma = min_at (F,m,n) by A1, A2, A3, Def11; :: thesis: verum

( ma = min_at (F,m,n) iff ( m <= ma & ma <= n & ( for i being Nat st m <= i & i <= n holds

F . ma <= F . i ) & ( for i being Nat st m <= i & i < ma holds

F . ma < F . i ) ) )

let m, n, ma be Nat; :: thesis: ( 1 <= m & m <= n & n <= len F implies ( ma = min_at (F,m,n) iff ( m <= ma & ma <= n & ( for i being Nat st m <= i & i <= n holds

F . ma <= F . i ) & ( for i being Nat st m <= i & i < ma holds

F . ma < F . i ) ) ) )

assume that

A1: 1 <= m and

A2: m <= n and

A3: n <= len F ; :: thesis: ( ma = min_at (F,m,n) iff ( m <= ma & ma <= n & ( for i being Nat st m <= i & i <= n holds

F . ma <= F . i ) & ( for i being Nat st m <= i & i < ma holds

F . ma < F . i ) ) )

set Cut = (m,n) -cut F;

A4: (len ((m,n) -cut F)) + m = n + 1 by A1, A2, A3, Def1;

hereby :: thesis: ( m <= ma & ma <= n & ( for i being Nat st m <= i & i <= n holds

F . ma <= F . i ) & ( for i being Nat st m <= i & i < ma holds

F . ma < F . i ) implies ma = min_at (F,m,n) )

set Cut = (m,n) -cut F;F . ma <= F . i ) & ( for i being Nat st m <= i & i < ma holds

F . ma < F . i ) implies ma = min_at (F,m,n) )

A5:
n - m < (n - m) + 1
by XREAL_1:29;

assume ma = min_at (F,m,n) ; :: thesis: ( m <= ma & ma <= n & ( for i being Nat st m <= i & i <= n holds

F . ma <= F . i ) & ( for i being Nat st m <= i & i < ma holds

F . ma < F . i ) )

then consider X being non empty finite Subset of INT such that

A6: X = rng ((m,n) -cut F) and

A7: ma + 1 = ((min X) .. ((m,n) -cut F)) + m by A1, A2, A3, Def11;

A8: ma = (((min X) .. ((m,n) -cut F)) - 1) + m by A7;

A9: ma = (((min X) .. ((m,n) -cut F)) + m) - 1 by A7;

A10: min X in X by XXREAL_2:def 7;

then A11: 1 <= (min X) .. ((m,n) -cut F) by A6, FINSEQ_4:21;

then 1 - 1 <= ((min X) .. ((m,n) -cut F)) - 1 by XREAL_1:9;

then reconsider i1 = ((min X) .. ((m,n) -cut F)) - 1 as Element of NAT by INT_1:3;

A12: (min X) .. ((m,n) -cut F) <= len ((m,n) -cut F) by A6, A10, FINSEQ_4:21;

then i1 < len ((m,n) -cut F) by XREAL_1:146, XXREAL_0:2;

then A13: F . ma = ((m,n) -cut F) . (i1 + 1) by A1, A2, A3, A8, Def1

.= ((m,n) -cut F) . ((ma + 1) - m) by A7 ;

((min X) .. ((m,n) -cut F)) + m <= (len ((m,n) -cut F)) + m by A12, XREAL_1:6;

then A14: ma <= ((len ((m,n) -cut F)) + m) - 1 by A9, XREAL_1:9;

m + 1 <= ((min X) .. ((m,n) -cut F)) + m by A11, XREAL_1:6;

then (m + 1) - 1 <= ma by A9, XREAL_1:9;

hence ( m <= ma & ma <= n ) by A4, A14; :: thesis: ( ( for i being Nat st m <= i & i <= n holds

F . ma <= F . i ) & ( for i being Nat st m <= i & i < ma holds

F . ma < F . i ) )

A15: ((m,n) -cut F) . ((min X) .. ((m,n) -cut F)) = min X by A6, A10, FINSEQ_4:19;

thus A16: for i being Nat st m <= i & i <= n holds

F . ma <= F . i :: thesis: for i being Nat st m <= i & i < ma holds

F . ma < F . i

assume that

A23: m <= i and

A24: i < ma ; :: thesis: F . ma < F . i

A25: i <= n by A4, A14, A24, XXREAL_0:2;

then A26: F . ma <= F . i by A16, A23;

m - m <= i - m by A23, XREAL_1:9;

then reconsider i1 = i - m as Element of NAT by INT_1:3;

reconsider k = i1 + 1 as Element of NAT ;

i <= ((len ((m,n) -cut F)) - 1) + m by A14, A24, XXREAL_0:2;

then i - m <= (len ((m,n) -cut F)) - 1 by XREAL_1:20;

then A27: k <= len ((m,n) -cut F) by XREAL_1:19;

i1 <= n - m by A25, XREAL_1:9;

then A28: i1 < len ((m,n) -cut F) by A4, A5, XXREAL_0:2;

0 + 1 <= k by XREAL_1:6;

then A29: k in dom ((m,n) -cut F) by A27, FINSEQ_3:25;

i - m < ma - m by A24, XREAL_1:9;

then A30: k < (ma - m) + 1 by XREAL_1:6;

F . i = F . (i1 + m)

.= ((m,n) -cut F) . k by A1, A2, A3, A28, Def1 ;

then F . i <> F . ma by A6, A7, A10, A13, A30, A29, FINSEQ_4:19, FINSEQ_4:24;

hence F . ma < F . i by A26, XXREAL_0:1; :: thesis: verum

end;assume ma = min_at (F,m,n) ; :: thesis: ( m <= ma & ma <= n & ( for i being Nat st m <= i & i <= n holds

F . ma <= F . i ) & ( for i being Nat st m <= i & i < ma holds

F . ma < F . i ) )

then consider X being non empty finite Subset of INT such that

A6: X = rng ((m,n) -cut F) and

A7: ma + 1 = ((min X) .. ((m,n) -cut F)) + m by A1, A2, A3, Def11;

A8: ma = (((min X) .. ((m,n) -cut F)) - 1) + m by A7;

A9: ma = (((min X) .. ((m,n) -cut F)) + m) - 1 by A7;

A10: min X in X by XXREAL_2:def 7;

then A11: 1 <= (min X) .. ((m,n) -cut F) by A6, FINSEQ_4:21;

then 1 - 1 <= ((min X) .. ((m,n) -cut F)) - 1 by XREAL_1:9;

then reconsider i1 = ((min X) .. ((m,n) -cut F)) - 1 as Element of NAT by INT_1:3;

A12: (min X) .. ((m,n) -cut F) <= len ((m,n) -cut F) by A6, A10, FINSEQ_4:21;

then i1 < len ((m,n) -cut F) by XREAL_1:146, XXREAL_0:2;

then A13: F . ma = ((m,n) -cut F) . (i1 + 1) by A1, A2, A3, A8, Def1

.= ((m,n) -cut F) . ((ma + 1) - m) by A7 ;

((min X) .. ((m,n) -cut F)) + m <= (len ((m,n) -cut F)) + m by A12, XREAL_1:6;

then A14: ma <= ((len ((m,n) -cut F)) + m) - 1 by A9, XREAL_1:9;

m + 1 <= ((min X) .. ((m,n) -cut F)) + m by A11, XREAL_1:6;

then (m + 1) - 1 <= ma by A9, XREAL_1:9;

hence ( m <= ma & ma <= n ) by A4, A14; :: thesis: ( ( for i being Nat st m <= i & i <= n holds

F . ma <= F . i ) & ( for i being Nat st m <= i & i < ma holds

F . ma < F . i ) )

A15: ((m,n) -cut F) . ((min X) .. ((m,n) -cut F)) = min X by A6, A10, FINSEQ_4:19;

thus A16: for i being Nat st m <= i & i <= n holds

F . ma <= F . i :: thesis: for i being Nat st m <= i & i < ma holds

F . ma < F . i

proof

let i be Nat; :: thesis: ( m <= i & i < ma implies F . ma < F . i )
let i be Nat; :: thesis: ( m <= i & i <= n implies F . ma <= F . i )

assume that

A17: m <= i and

A18: i <= n ; :: thesis: F . ma <= F . i

m - m <= i - m by A17, XREAL_1:9;

then reconsider i1 = i - m as Element of NAT by INT_1:3;

A19: 0 + 1 <= i1 + 1 by XREAL_1:6;

A20: n - m < (n - m) + 1 by XREAL_1:29;

i1 <= n - m by A18, XREAL_1:9;

then A21: i1 < len ((m,n) -cut F) by A4, A20, XXREAL_0:2;

then i1 + 1 <= len ((m,n) -cut F) by NAT_1:13;

then A22: i1 + 1 in dom ((m,n) -cut F) by A19, FINSEQ_3:25;

((m,n) -cut F) . (i1 + 1) = F . (m + i1) by A1, A2, A3, A21, Def1;

then F . i in rng ((m,n) -cut F) by A22, FUNCT_1:def 3;

hence F . ma <= F . i by A6, A7, A13, A15, XXREAL_2:def 7; :: thesis: verum

end;assume that

A17: m <= i and

A18: i <= n ; :: thesis: F . ma <= F . i

m - m <= i - m by A17, XREAL_1:9;

then reconsider i1 = i - m as Element of NAT by INT_1:3;

A19: 0 + 1 <= i1 + 1 by XREAL_1:6;

A20: n - m < (n - m) + 1 by XREAL_1:29;

i1 <= n - m by A18, XREAL_1:9;

then A21: i1 < len ((m,n) -cut F) by A4, A20, XXREAL_0:2;

then i1 + 1 <= len ((m,n) -cut F) by NAT_1:13;

then A22: i1 + 1 in dom ((m,n) -cut F) by A19, FINSEQ_3:25;

((m,n) -cut F) . (i1 + 1) = F . (m + i1) by A1, A2, A3, A21, Def1;

then F . i in rng ((m,n) -cut F) by A22, FUNCT_1:def 3;

hence F . ma <= F . i by A6, A7, A13, A15, XXREAL_2:def 7; :: thesis: verum

assume that

A23: m <= i and

A24: i < ma ; :: thesis: F . ma < F . i

A25: i <= n by A4, A14, A24, XXREAL_0:2;

then A26: F . ma <= F . i by A16, A23;

m - m <= i - m by A23, XREAL_1:9;

then reconsider i1 = i - m as Element of NAT by INT_1:3;

reconsider k = i1 + 1 as Element of NAT ;

i <= ((len ((m,n) -cut F)) - 1) + m by A14, A24, XXREAL_0:2;

then i - m <= (len ((m,n) -cut F)) - 1 by XREAL_1:20;

then A27: k <= len ((m,n) -cut F) by XREAL_1:19;

i1 <= n - m by A25, XREAL_1:9;

then A28: i1 < len ((m,n) -cut F) by A4, A5, XXREAL_0:2;

0 + 1 <= k by XREAL_1:6;

then A29: k in dom ((m,n) -cut F) by A27, FINSEQ_3:25;

i - m < ma - m by A24, XREAL_1:9;

then A30: k < (ma - m) + 1 by XREAL_1:6;

F . i = F . (i1 + m)

.= ((m,n) -cut F) . k by A1, A2, A3, A28, Def1 ;

then F . i <> F . ma by A6, A7, A10, A13, A30, A29, FINSEQ_4:19, FINSEQ_4:24;

hence F . ma < F . i by A26, XXREAL_0:1; :: thesis: verum

A31: (len ((m,n) -cut F)) + m = n + 1 by A1, A2, A3, Def1;

then A32: len ((m,n) -cut F) = (n + 1) - m ;

set X = rng ((m,n) -cut F);

A33: rng ((m,n) -cut F) is Subset of INT ;

m < n + 1 by A2, NAT_1:13;

then m - m < (n + 1) - m by XREAL_1:9;

then not (m,n) -cut F is empty by A31;

then reconsider X = rng ((m,n) -cut F) as non empty finite Subset of INT by A33;

reconsider rX = X as non empty finite Subset of REAL by MEMBERED:3;

assume that

A34: m <= ma and

A35: ma <= n and

A36: for i being Nat st m <= i & i <= n holds

F . ma <= F . i and

A37: for i being Nat st m <= i & i < ma holds

F . ma < F . i ; :: thesis: ma = min_at (F,m,n)

m - m <= ma - m by A34, XREAL_1:9;

then reconsider qm = ma - m as Element of NAT by INT_1:3;

A38: qm + 1 = (ma + 1) - m ;

then reconsider q1 = (ma + 1) - m as Element of NAT ;

ma + 1 <= n + 1 by A35, XREAL_1:6;

then A39: q1 <= len ((m,n) -cut F) by A32, XREAL_1:9;

0 + 1 <= qm + 1 by XREAL_1:6;

then A40: q1 in dom ((m,n) -cut F) by A39, FINSEQ_3:25;

A41: ma = qm + m ;

qm < len ((m,n) -cut F) by A38, A39, NAT_1:13;

then A42: F . ma = ((m,n) -cut F) . ((ma + 1) - m) by A1, A2, A3, A38, A41, Def1;

now :: thesis: ( F . ma in X & ( for k being ExtReal st k in X holds

F . ma <= k ) )

then A47:
F . ma = min rX
by XXREAL_2:def 7;F . ma <= k ) )

thus
F . ma in X
by A40, A42, FUNCT_1:def 3; :: thesis: for k being ExtReal st k in X holds

F . ma <= k

let k be ExtReal; :: thesis: ( k in X implies F . ma <= k )

assume k in X ; :: thesis: F . ma <= k

then consider dk being object such that

A43: dk in dom ((m,n) -cut F) and

A44: ((m,n) -cut F) . dk = k by FUNCT_1:def 3;

reconsider dk = dk as Element of NAT by A43;

1 <= dk by A43, FINSEQ_3:25;

then 1 - 1 <= dk - 1 by XREAL_1:9;

then reconsider dk1 = dk - 1 as Element of NAT by INT_1:3;

A45: dk <= len ((m,n) -cut F) by A43, FINSEQ_3:25;

then dk + m <= (len ((m,n) -cut F)) + m by XREAL_1:6;

then A46: (dk + m) - 1 <= n by A4, XREAL_1:20;

dk1 < len ((m,n) -cut F) by A45, XREAL_1:146, XXREAL_0:2;

then F . (dk1 + m) = ((m,n) -cut F) . (dk1 + 1) by A1, A2, A3, Def1

.= ((m,n) -cut F) . dk ;

hence F . ma <= k by A36, A44, A46, NAT_1:12; :: thesis: verum

end;F . ma <= k

let k be ExtReal; :: thesis: ( k in X implies F . ma <= k )

assume k in X ; :: thesis: F . ma <= k

then consider dk being object such that

A43: dk in dom ((m,n) -cut F) and

A44: ((m,n) -cut F) . dk = k by FUNCT_1:def 3;

reconsider dk = dk as Element of NAT by A43;

1 <= dk by A43, FINSEQ_3:25;

then 1 - 1 <= dk - 1 by XREAL_1:9;

then reconsider dk1 = dk - 1 as Element of NAT by INT_1:3;

A45: dk <= len ((m,n) -cut F) by A43, FINSEQ_3:25;

then dk + m <= (len ((m,n) -cut F)) + m by XREAL_1:6;

then A46: (dk + m) - 1 <= n by A4, XREAL_1:20;

dk1 < len ((m,n) -cut F) by A45, XREAL_1:146, XXREAL_0:2;

then F . (dk1 + m) = ((m,n) -cut F) . (dk1 + 1) by A1, A2, A3, Def1

.= ((m,n) -cut F) . dk ;

hence F . ma <= k by A36, A44, A46, NAT_1:12; :: thesis: verum

set mX = min X;

set mXC = (min X) .. ((m,n) -cut F);

A48: min X in X by XXREAL_2:def 7;

then 1 <= (min X) .. ((m,n) -cut F) by FINSEQ_4:21;

then 1 - 1 <= ((min X) .. ((m,n) -cut F)) - 1 by XREAL_1:9;

then reconsider mXC1 = ((min X) .. ((m,n) -cut F)) - 1 as Element of NAT by INT_1:3;

set mXCm = mXC1 + m;

(min X) .. ((m,n) -cut F) <= len ((m,n) -cut F) by A48, FINSEQ_4:21;

then A49: mXC1 < len ((m,n) -cut F) by XREAL_1:146, XXREAL_0:2;

(min X) .. ((m,n) -cut F) = mXC1 + 1 ;

then A50: F . (mXC1 + m) = ((m,n) -cut F) . ((min X) .. ((m,n) -cut F)) by A1, A2, A3, A49, Def1;

A51: m <= mXC1 + m by NAT_1:12;

A52: ((m,n) -cut F) . ((min X) .. ((m,n) -cut F)) = min X by A48, FINSEQ_4:19;

now :: thesis: not q1 <> (min X) .. ((m,n) -cut F)

then
ma + 1 = ((min X) .. ((m,n) -cut F)) + m
;assume A53:
q1 <> (min X) .. ((m,n) -cut F)
; :: thesis: contradiction

end;hence ma = min_at (F,m,n) by A1, A2, A3, Def11; :: thesis: verum