theorem :: ZMODLAT1:89

for V, W being non empty right_zeroed ModuleStr over INT.Ring
for f being FrForm of V,W st ( f is additiveFAF or f is additiveSAF ) holds
( f is constant iff for v being Vector of V
for w being Vector of W holds f . (v,w) = 0. INT.Ring )