theorem :: ZMODLAT1:43

for V, W being non empty ModuleStr over INT.Ring
for a, b being Element of F_Real
for f being FrForm of V,W holds (a + b) * f = (a * f) + (b * f)