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