theorem HTh25: :: ZMODLAT1:73

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