theorem :: BILINEAR:22

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