theorem :: ZMODLAT1:71

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