theorem HTh12: :: ZMODLAT1:60

for V, W being non empty ModuleStr over INT.Ring
for f, g being FrForm of V,W
for w being Vector of W holds FrFunctionalSAF ((f + g),w) = (FrFunctionalSAF (f,w)) + (FrFunctionalSAF (g,w))