theorem :: ZMODLAT1:44

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 * (b * f)