for V being RealLinearSpace
for f being Functional of V
for s being FinSequence of V st f is additive holds
f . (Sum s) = Sum (f * s)