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