:: deftheorem Def2 defines + BILINEAR:def 2 :
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)) );