let F be FinSequence of INT ; :: thesis:
let m, n, ma be Element of NAT ; :: thesis:
assume A1: ( 1 <= m & m <= n & n <= len F ) ; :: thesis:
set Cut = m,n -cut F;
A2: (len (m,n -cut F)) + m = n + 1 by A1, Def1;

hereby :: thesis:

assume ma = min_at F,m,n ; :: thesis:
then consider X being non empty finite Subset of INT such that
A3: X = rng (m,n -cut F) and
A4: ma + 1 = ((min X) .. (m,n -cut F)) + m by A1, Def12;
A5: ma = (((min X) .. (m,n -cut F)) + m) - 1 by A4;
A6: min X in X by XXREAL_2:def 7;
then A7: ( 1 <= (min X) .. (m,n -cut F) & (min X) .. (m,n -cut F) <= len (m,n -cut F) ) by A3, FINSEQ_4:31;
then m + 1 <= ((min X) .. (m,n -cut F)) + m by XREAL_1:8;
then A8: (m + 1) - 1 <= ma by A5, XREAL_1:11;
((min X) .. (m,n -cut F)) + m <= (len (m,n -cut F)) + m by A7, XREAL_1:8;
then A9: ma <= ((len (m,n -cut F)) + m) - 1 by A5, XREAL_1:11;
hence ( m <= ma & ma <= n ) by A2, A8; :: thesis:
1 - 1 <= ((min X) .. (m,n -cut F)) - 1 by A7, XREAL_1:11;
then reconsider i1 = ((min X) .. (m,n -cut F)) - 1 as Element of NAT by INT_1:16;
A10: ma = (((min X) .. (m,n -cut F)) - 1) + m by A4;
i1 < len (m,n -cut F) by A7, XREAL_1:148, XXREAL_0:2;
then A11: F . ma = (m,n -cut F) . (i1 + 1) by A1, A10, Def1
.= (m,n -cut F) . ((ma + 1) - m) by A4 ;
A12: (m,n -cut F) . ((min X) .. (m,n -cut F)) = min X by A3, A6, FINSEQ_4:29;
thus A13: for i being Element of NAT st m <= i & i <= n holds
F . ma <= F . i :: thesis:

let i be Element of NAT ; :: thesis:
assume A14: ( m <= i & i <= n ) ; :: thesis:
then m - m <= i - m by XREAL_1:11;
then reconsider i1 = i - m as Element of NAT by INT_1:16;
( n - m < (n - m) + 1 & i1 <= n - m ) by A14, XREAL_1:11, XREAL_1:31;
then A15: i1 < len (m,n -cut F) by A2, XXREAL_0:2;
then A16: (m,n -cut F) . (i1 + 1) = F . (m + i1) by A1, Def1;
A17: 0 + 1 <= i1 + 1 by XREAL_1:8;
i1 + 1 <= len (m,n -cut F) by A15, NAT_1:13;
then i1 + 1 in dom (m,n -cut F) by A17, FINSEQ_3:27;
then F . i in rng (m,n -cut F) by A16, FUNCT_1:def 5;
hence F . ma <= F . i by A3, A4, A11, A12, XXREAL_2:def 7; :: thesis:

end;

let i be Element of NAT ; :: thesis:
assume A18: ( m <= i & i < ma ) ; :: thesis:
then A19: i <= n by A2, A9, XXREAL_0:2;
m - m <= i - m by A18, XREAL_1:11;
then reconsider i1 = i - m as Element of NAT by INT_1:16;
reconsider k = i1 + 1 as Element of NAT ;
i - m < ma - m by A18, XREAL_1:11;
then A20: k < (ma - m) + 1 by XREAL_1:8;
A21: 0 + 1 <= k by XREAL_1:8;
i <= ((len (m,n -cut F)) - 1) + m by A9, A18, XXREAL_0:2;
then i - m <= (len (m,n -cut F)) - 1 by XREAL_1:22;
then k <= len (m,n -cut F) by XREAL_1:21;
then A22: k in dom (m,n -cut F) by A21, FINSEQ_3:27;
( n - m < (n - m) + 1 & i1 <= n - m ) by A19, XREAL_1:11, XREAL_1:31;
then A23: i1 < len (m,n -cut F) by A2, XXREAL_0:2;
F . i = F . (i1 + m)
.= (m,n -cut F) . k by A1, A23, Def1 ;
then A24: F . i <> F . ma by A3, A4, A6, A11, A20, A22, FINSEQ_4:29, FINSEQ_4:34;
F . ma <= F . i by A13, A18, A19;
hence F . ma < F . i by A24, XXREAL_0:1; :: thesis:

end;

assume that
A25: ( m <= ma & ma <= n ) and
A26: for i being Element of NAT st m <= i & i <= n holds
F . ma <= F . i and
A27: for i being Element of NAT st m <= i & i < ma holds
F . ma < F . i ; :: thesis:
set Cut = m,n -cut F;
set X = rng (m,n -cut F);
A28: rng (m,n -cut F) is Subset of INT ;
A29: m < n + 1 by A1, NAT_1:13;
A30: (len (m,n -cut F)) + m = n + 1 by A1, Def1;
then A31: len (m,n -cut F) = (n + 1) - m ;
m - m < (n + 1) - m by A29, XREAL_1:11;
then not m,n -cut F is empty by A30;
then reconsider X = rng (m,n -cut F) as non empty finite Subset of INT by A28;
set mX = min X;
reconsider rX = X as non empty finite Subset of REAL by MEMBERED:3;
A32: min X in X by XXREAL_2:def 7;
then A33: (m,n -cut F) . ((min X) .. (m,n -cut F)) = min X by FINSEQ_4:29;
m - m <= ma - m by A25, XREAL_1:11;
then reconsider qm = ma - m as Element of NAT by INT_1:16;
A34: qm + 1 = (ma + 1) - m ;
then reconsider q1 = (ma + 1) - m as Element of NAT ;
set mXC = (min X) .. (m,n -cut F);
A35: 0 + 1 <= qm + 1 by XREAL_1:8;
ma + 1 <= n + 1 by A25, XREAL_1:8;
then A36: q1 <= len (m,n -cut F) by A31, XREAL_1:11;
then A37: q1 in dom (m,n -cut F) by A35, FINSEQ_3:27;
A38: qm < len (m,n -cut F) by A34, A36, NAT_1:13;
ma = qm + m ;
then A39: F . ma = (m,n -cut F) . ((ma + 1) - m) by A1, A34, A38, Def1;

thus F . ma in X by A37, A39, FUNCT_1:def 5; :: thesis:
let k be ext-real number ; :: thesis:
assume k in X ; :: thesis:
then consider dk being set such that
A40: ( dk in dom (m,n -cut F) & (m,n -cut F) . dk = k ) by FUNCT_1:def 5;
reconsider dk = dk as Element of NAT by A40;
A41: ( 1 <= dk & dk <= len (m,n -cut F) ) by A40, FINSEQ_3:27;
then 1 - 1 <= dk - 1 by XREAL_1:11;
then reconsider dk1 = dk - 1 as Element of NAT by INT_1:16;
dk + m <= (len (m,n -cut F)) + m by A41, XREAL_1:8;
then A42: (dk + m) - 1 <= n by A2, XREAL_1:22;
dk1 < len (m,n -cut F) by A41, XREAL_1:148, XXREAL_0:2;
then F . (dk1 + m) = (m,n -cut F) . (dk1 + 1) by A1, Def1
.= (m,n -cut F) . dk ;
hence F . ma <= k by A26, A40, A42, NAT_1:12; :: thesis:

end;

then A43: F . ma = min rX by XXREAL_2:def 7;
1 <= (min X) .. (m,n -cut F) by A32, FINSEQ_4:31;
then 1 - 1 <= ((min X) .. (m,n -cut F)) - 1 by XREAL_1:11;
then reconsider mXC1 = ((min X) .. (m,n -cut F)) - 1 as Element of NAT by INT_1:16;
set mXCm = mXC1 + m;
A44: m <= mXC1 + m by NAT_1:12;
A45: (min X) .. (m,n -cut F) = mXC1 + 1 ;
( mXC1 < (min X) .. (m,n -cut F) & (min X) .. (m,n -cut F) <= len (m,n -cut F) ) by A32, FINSEQ_4:31, XREAL_1:148;
then mXC1 < len (m,n -cut F) by XXREAL_0:2;
then A46: F . (mXC1 + m) = (m,n -cut F) . ((min X) .. (m,n -cut F)) by A1, A45, Def1;

assume A47: q1 <> (min X) .. (m,n -cut F) ; :: thesis:

per cases by A47, XXREAL_0:1;

suppose q1 < (min X) .. (m,n -cut F) ; :: thesis:

hence contradiction by A37, A39, A43, FINSEQ_4:34; :: thesis:

end;

suppose q1 > (min X) .. (m,n -cut F) ; :: thesis:

then ((min X) .. (m,n -cut F)) + m < ma + 1 by XREAL_1:22;
then (((min X) .. (m,n -cut F)) + m) - 1 < ma by XREAL_1:21;
hence contradiction by A27, A33, A43, A44, A46; :: thesis:

end;

then ma + 1 = ((min X) .. (m,n -cut F)) + m ;
hence ma = min_at F,m,n by A1, Def12; :: thesis: