for F, G being FinSequence of ExtREAL
for a being R_eal st ( a is real or for i being Nat st i in dom F holds
F . i < 0. or for i being Nat st i in dom F holds
0. < F . i ) & dom F = dom G & ( for i being Nat st i in dom G holds
G . i = a * (F . i) ) holds
Sum G = a * (Sum F)