let r be real number ; :: 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 Lm4;
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 Th16, Th22, SETWOP_2:41
.= r * (Sum F1) by Lm3
.= r * (Sum F) ; :: thesis: verum