theorem :: ZMATRLIN:60

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