theorem HTh30: :: ZMODLAT1:79

for V, W being non empty right_zeroed ModuleStr over INT.Ring
for f being additiveSAF FrForm of V,W
for w being Vector of W holds f . ((0. V),w) = 0. INT.Ring