:: deftheorem Def11 defines additiveFAF BILINEAR:def 11 :
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 additiveFAF iff for v being Vector of V holds FunctionalFAF (f,v) is additive );