:: deftheorem HDef12 defines additiveSAF ZMODLAT1:def 28 :
for V, W being non empty ModuleStr over INT.Ring
for f being FrForm of V,W holds
( f is additiveSAF iff for w being Vector of W holds FrFunctionalSAF (f,w) is additive );