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