:: deftheorem Def10 defines FormFunctional BILINEAR:def 10 :
for K being non empty multMagma
for V, W being non empty ModuleStr over K
for f being Functional of V
for g being Functional of W
for b₆ being Form of V,W holds
( b₆ = FormFunctional (f,g) iff for v being Vector of V
for w being Vector of W holds b₆ . (v,w) = (f . v) * (g . w) );