theorem Th40: :: BILINEAR:40

for K being non empty right_complementable add-associative right_zeroed doubleLoopStr
for V, W being non empty right_zeroed ModuleStr over K
for f being Form of V,W st ( f is additiveFAF or f is additiveSAF ) holds
( f is constant iff for v being Vector of V
for w being Vector of W holds f . (v,w) = 0. K )