theorem :: ZMODLAT1:45

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