theorem :: BILINEAR:23

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 holds FormFunctional ((0Functional V),g) = NulForm (V,W)