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