theorem :: ZMODLAT1:70

for V, W being non empty ModuleStr over INT.Ring
for f being FrFunctional of V holds FrFormFunctional (f,(0FrFunctional W)) = NulFrForm (V,W)