let f be real-valued FinSequence; :: thesis: for a being Real st len f > 0 & a > 0 holds
( max (a * f) = a * (max f) & max_p (a * f) = max_p f )
let a be Real; :: thesis: ( len f > 0 & a > 0 implies ( max (a * f) = a * (max f) & max_p (a * f) = max_p f ) )
assume that
A1: len f > 0 and
A2: a > 0 ; :: thesis: ( max (a * f) = a * (max f) & max_p (a * f) = max_p f )
A3: len (a * f) = len f by RVSUM_1:117;
then A4: max_p (a * f) in dom (a * f) by A1, Def1;
then ( 1 <= max_p (a * f) & max_p (a * f) <= len (a * f) ) by FINSEQ_3:25;
then max_p (a * f) in Seg (len f) by A3, FINSEQ_1:1;
then A5: max_p (a * f) in dom f by FINSEQ_1:def 3;
then f . (max_p f) >= f . (max_p (a * f)) by A1, Def1;
then A6: a * (f . (max_p f)) >= a * (f . (max_p (a * f))) by A2, XREAL_1:64;
A7: ( a * (f . (max_p f)) = (a * f) . (max_p f) & a * (f . (max_p (a * f))) = (a * f) . (max_p (a * f)) ) by RVSUM_1:44;
A8: dom (a * f) = dom f by VALUED_1:def 5;
then A9: max_p f in dom (a * f) by A1, Def1;
then (a * f) . (max_p f) <= (a * f) . (max_p (a * f)) by A1, A3, Def1;
then A10: f . (max_p f) <= f . (max_p (a * f)) by A2, A7, XREAL_1:68;
f . (max_p (a * f)) <= f . (max_p f) by A1, A5, Def1;
then f . (max_p f) = f . (max_p (a * f)) by A10, XXREAL_0:1;
then A11: ( max (a * f) = a * (f . (max_p (a * f))) & max_p (a * f) >= max_p f ) by A1, A8, A4, Def1, RVSUM_1:44;
max_p f in dom (a * f) by A1, A8, Def1;
then (a * f) . (max_p (a * f)) >= (a * f) . (max_p f) by A1, A3, Def1;
then (a * f) . (max_p (a * f)) = (a * f) . (max_p f) by A7, A6, XXREAL_0:1;
then max_p (a * f) <= max_p f by A1, A3, A9, Def1;
hence ( max (a * f) = a * (max f) & max_p (a * f) = max_p f ) by A11, XXREAL_0:1; :: thesis: verum