:: deftheorem BLDef12 defines additiveSAF ZMATRLIN:def 23 :
for V, W being non empty ModuleStr over INT.Ring
for f being Form of V,W holds
( f is additiveSAF iff for w being Vector of W holds FunctionalSAF (f,w) is additive );