theorem :: ZMODLAT1:42

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