:: deftheorem Def7 defines - BILINEAR:def 7 :
for K being non empty addLoopStr
for V, W being non empty ModuleStr over K
for f, g, b₆ being Form of V,W holds
( b₆ = f - g iff for v being Vector of V
for w being Vector of W holds b₆ . (v,w) = (f . (v,w)) - (g . (v,w)) );