theorem Th20: :: BILINEAR:20

for K being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
for V, W being non empty ModuleStr over K
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. K