theorem HTh27: :: ZMODLAT1:76

for V, W being non empty ModuleStr over INT.Ring
for v being Vector of V
for u, w being Vector of W
for f being FrForm of V,W st f is additiveFAF holds
f . (v,(u + w)) = (f . (v,u)) + (f . (v,w))