theorem :: ZMATRLIN:81
for V, W being non empty ModuleStr over INT.Ring
for f being Functional of V holds FormFunctional (f,(0Functional W)) = NulForm (V,W)