theorem BLTh20: :: ZMATRLIN:79

for V, W being non empty ModuleStr over INT.Ring
for f being Functional of V
for v being Vector of V
for w being Vector of W holds (FormFunctional (f,(0Functional W))) . (v,w) = 0