theorem HTh10: :: ZMODLAT1:58

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