for r being Real
for Fr1, Fr2 being XFinSequence of REAL st dom Fr1 = dom Fr2 & ( for n being Nat st n in len Fr1 holds
Fr1 . n = r * (Fr2 . n) ) holds
Sum Fr1 = r * (Sum Fr2)