let f be real-valued FinSequence; :: 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 RVSUM_1:114;
then A3: max_p (- f) in dom (- f) by A1, Def1;
then ( 1 <= max_p (- f) & max_p (- f) <= len (- f) ) by FINSEQ_3:25;
then max_p (- f) in Seg (len f) by A2, FINSEQ_1:1;
then A4: max_p (- f) in dom f by FINSEQ_1:def 3;
then f . (min_p f) <= f . (max_p (- f)) by A1, Def2;
then A5: - (f . (min_p f)) >= - (f . (max_p (- f))) by XREAL_1:24;
A6: ( - (f . (min_p f)) = (- f) . (min_p f) & - (f . (max_p (- f))) = (- f) . (max_p (- f)) ) by RVSUM_1:17;
A7: dom (- f) = dom f by VALUED_1:8;
then A8: min_p f in dom (- f) by A1, Def2;
then (- f) . (max_p (- f)) >= (- f) . (min_p f) by A1, A2, Def1;
then A9: f . (max_p (- f)) <= f . (min_p f) by A6, XREAL_1:24;
f . (min_p f) <= f . (max_p (- f)) by A1, A4, Def2;
then f . (min_p f) = f . (max_p (- f)) by A9, XXREAL_0:1;
then A10: ( max (- f) = - (f . (max_p (- f))) & max_p (- f) >= min_p f ) by A1, A7, A3, Def2, RVSUM_1:17;
min_p f in dom (- f) by A1, A7, Def2;
then (- f) . (max_p (- f)) >= (- f) . (min_p f) by A1, A2, Def1;
then (- f) . (max_p (- f)) = (- f) . (min_p f) by A6, A5, XXREAL_0:1;
then max_p (- f) <= min_p f by A1, A2, A8, Def1;
hence ( max (- f) = - (min f) & max_p (- f) = min_p f ) by A10, XXREAL_0:1; :: thesis: verum