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;
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) )
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 ;
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 ;
then i1 < len ((m,n) -cut F) by ;
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 ;
then A14: ma <= ((len ((m,n) -cut F)) + m) - 1 by ;
m + 1 <= ((min X) .. ((m,n) -cut F)) + m by ;
then (m + 1) - 1 <= ma by ;
hence ( m <= ma & ma <= n ) by ; :: 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 ;
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 <= 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 ;
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 ;
then A21: i1 < len ((m,n) -cut F) by ;
then i1 + 1 <= len ((m,n) -cut F) by NAT_1:13;
then A22: i1 + 1 in dom ((m,n) -cut F) by ;
((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 ;
hence F . ma <= F . i by ; :: thesis: verum
end;
let i be Nat; :: thesis: ( m <= i & i < ma implies F . ma < F . i )
assume that
A23: m <= i and
A24: i < ma ; :: thesis: F . ma < F . i
A25: i <= n by ;
then A26: F . ma <= F . i by ;
m - m <= i - m by ;
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 ;
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 ;
then A28: i1 < len ((m,n) -cut F) by ;
0 + 1 <= k by XREAL_1:6;
then A29: k in dom ((m,n) -cut F) by ;
i - m < ma - m by ;
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 ;
hence F . ma < F . i by ; :: thesis: verum
end;
set Cut = (m,n) -cut F;
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 ;
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 ;
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 ;
then A39: q1 <= len ((m,n) -cut F) by ;
0 + 1 <= qm + 1 by XREAL_1:6;
then A40: q1 in dom ((m,n) -cut F) by ;
A41: ma = qm + m ;
qm < len ((m,n) -cut F) by ;
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 ) )
thus F . ma in X by ; :: 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 ;
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 ;
then dk + m <= (len ((m,n) -cut F)) + m by XREAL_1:6;
then A46: (dk + m) - 1 <= n by ;
dk1 < len ((m,n) -cut F) by ;
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 ; :: thesis: verum
end;
then A47: F . ma = min rX by XXREAL_2:def 7;
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 ;
then A49: mXC1 < len ((m,n) -cut F) by ;
(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 ;
now :: thesis: not q1 <> (min X) .. ((m,n) -cut F)
assume A53: q1 <> (min X) .. ((m,n) -cut F) ; :: thesis: contradiction
per cases ( q1 < (min X) .. ((m,n) -cut F) or q1 > (min X) .. ((m,n) -cut F) ) by ;
suppose q1 > (min X) .. ((m,n) -cut F) ; :: thesis: contradiction
then ((min X) .. ((m,n) -cut F)) + m < ma + 1 by XREAL_1:20;
then (((min X) .. ((m,n) -cut F)) + m) - 1 < ma by XREAL_1:19;
hence contradiction by A37, A52, A47, A51, A50; :: thesis: verum
end;
end;
end;
then ma + 1 = ((min X) .. ((m,n) -cut F)) + m ;
hence ma = min_at (F,m,n) by A1, A2, A3, Def11; :: thesis: verum