theorem Th21: :: BILINEAR:21

for K being non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr
for V, W being non empty ModuleStr over K
for g being Functional of W
for v being Vector of V
for w being Vector of W holds (FormFunctional ((0Functional V),g)) . (v,w) = 0. K