:: deftheorem Def3 defines * BILINEAR:def 3 :
for K being non empty multMagma
for V, W being non empty ModuleStr over K
for f being Form of V,W
for a being Element of K
for b₆ being Form of V,W holds
( b₆ = a * f iff for v being Vector of V
for w being Vector of W holds b₆ . (v,w) = a * (f . (v,w)) );