for m being non zero Nat
for r being Real
for w, u being FinSequence of REAL m st u = r (#) w holds
Sum u = r * (Sum w)