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