let f be FinSequence of REAL ; for n being Nat st n < len f holds
( max (f /^ n) <= max f & min (f /^ n) >= min f )
let n be Nat; ( n < len f implies ( max (f /^ n) <= max f & min (f /^ n) >= min f ) )
A1:
1 <= 1 + n
by NAT_1:12;
assume A2:
n < len f
; ( max (f /^ n) <= max f & min (f /^ n) >= min f )
then A3:
len (f /^ n) = (len f) - n
by RFINSEQ:def 1;
then A4:
len (f /^ n) > 0
by A2, XREAL_1:50;
then A5:
min_p (f /^ n) in dom (f /^ n)
by Def2;
then A6:
f . ((min_p (f /^ n)) + n) = min (f /^ n)
by A2, RFINSEQ:def 1;
min_p (f /^ n) <= len (f /^ n)
by A5, FINSEQ_3:25;
then A7:
(min_p (f /^ n)) + n <= ((len f) - n) + n
by A3, XREAL_1:7;
A8:
1 <= 1 + n
by NAT_1:12;
1 <= min_p (f /^ n)
by A5, FINSEQ_3:25;
then
1 + n <= (min_p (f /^ n)) + n
by XREAL_1:7;
then
1 <= (min_p (f /^ n)) + n
by A8, XXREAL_0:2;
then A9:
(min_p (f /^ n)) + n in dom f
by A7, FINSEQ_3:25;
A10:
max_p (f /^ n) in dom (f /^ n)
by A4, Def1;
then
max_p (f /^ n) <= len (f /^ n)
by FINSEQ_3:25;
then A11:
(max_p (f /^ n)) + n <= ((len f) - n) + n
by A3, XREAL_1:7;
1 <= max_p (f /^ n)
by A10, FINSEQ_3:25;
then
1 + n <= (max_p (f /^ n)) + n
by XREAL_1:7;
then
1 <= (max_p (f /^ n)) + n
by A1, XXREAL_0:2;
then A12:
(max_p (f /^ n)) + n in dom f
by A11, FINSEQ_3:25;
f . ((max_p (f /^ n)) + n) = max (f /^ n)
by A2, A10, RFINSEQ:def 1;
hence
( max (f /^ n) <= max f & min (f /^ n) >= min f )
by A2, A12, A9, A6, Def1, Def2; verum