theorem :: ZMODLAT1:41

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