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