let f be FinSequence of REAL ; ( len f > 0 implies ( max (- f) = - (min f) & max_p (- f) = min_p f ) )
assume A1:
len f > 0
; ( 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; verum