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