let f be FinSequence of REAL ; :: thesis: ( len f > 0 implies ( max (- f) = - (min f) & max_p (- f) = min_p f ) )
assume A1: len f > 0 ; :: thesis: ( max (- f) = - (min f) & max_p (- f) = min_p f )
A2: len (- f) = len f by EUCLID_2:5;
A3: dom (- f) = dom f by VALUED_1:8;
A4: max_p (- f) in dom (- f) by A1, A2, Def1;
then A5: ( 1 <= max_p (- f) & max_p (- f) <= len (- f) ) by FINSEQ_3:27;
A6: max (- f) = - (f . (max_p (- f))) by RVSUM_1:35;
A7: min_p f in dom (- f) by A1, A3, Def2;
A8: - (f . (min_p f)) = (- f) . (min_p f) by RVSUM_1:35;
A9: - (f . (max_p (- f))) = (- f) . (max_p (- f)) by RVSUM_1:35;
max_p (- f) in Seg (len f) by A2, A5, FINSEQ_1:3;
then A10: max_p (- f) in dom f by FINSEQ_1:def 3;
(- f) . (max_p (- f)) >= (- f) . (min_p f) by A1, A2, A7, Def1;
then A11: f . (max_p (- f)) <= f . (min_p f) by A8, A9, XREAL_1:26;
f . (min_p f) <= f . (max_p (- f)) by A1, A10, Def2;
then A12: f . (min_p f) = f . (max_p (- f)) by A11, XXREAL_0:1;
min_p f in dom (- f) by A1, A3, Def2;
then A13: (- f) . (max_p (- f)) >= (- f) . (min_p f) by A1, A2, Def1;
f . (min_p f) <= f . (max_p (- f)) by A1, A10, Def2;
then - (f . (min_p f)) >= - (f . (max_p (- f))) by XREAL_1:26;
then A14: (- f) . (max_p (- f)) = (- f) . (min_p f) by A8, A9, A13, XXREAL_0:1;
A15: max_p (- f) >= min_p f by A1, A3, A4, A12, Def2;
max_p (- f) <= min_p f by A1, A2, A7, A14, Def1;
hence ( max (- f) = - (min f) & max_p (- f) = min_p f ) by A6, A15, XXREAL_0:1; :: thesis: verum