let r be Real; :: thesis: for F being real-valued FinSequence holds Sum (r * F) = r * (Sum F)
let F be real-valued FinSequence; :: thesis: Sum (r * F) = r * (Sum F)
reconsider F1 = F as FinSequence of REAL by Lm2;
reconsider s = r as Element of REAL by XREAL_0:def 1;
set rM = multreal [;] (s,(id REAL));
thus Sum (r * F) = (multreal [;] (s,(id REAL))) . (addreal $$ F1) by Th3, Th8, SETWOP_2:30
.= r * (Sum F1) by Lm1
.= r * (Sum F) ; :: thesis: verum