let f be FinSequence of REAL ; :: thesis: for n being Nat st n < len f holds
( max (f /^ n) <= max f & min (f /^ n) >= min f )
let n be Nat; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: verum