theorem :: ZMODLAT1:53

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