theorem HTh24: :: ZMODLAT1:72

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