:: deftheorem Def12 defines additiveSAF BILINEAR:def 12 :
for K being non empty addLoopStr
for V, W being non empty ModuleStr over K
for f being Form of V,W holds
( f is additiveSAF iff for w being Vector of W holds FunctionalSAF (f,w) is additive );