theorem :: ZMODLAT1:66

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))