theorem :: ZMODLAT1:52
for V being non empty ModuleStr over INT.Ring
for r, s being Element of F_Real
for f being FrFunctional of V holds (r + s) * f = (r * f) + (s * f)