theorem :: ZMODLAT1:39

for V, W being non empty ModuleStr over INT.Ring
for f being FrForm of V,W holds f + (NulFrForm (V,W)) = f