theorem HTh11: :: ZMODLAT1:59

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