theorem BLTh24: :: ZMATRLIN:83

for V, W being non empty ModuleStr over INT.Ring
for f being Functional of V
for g being Functional of W
for v being Vector of V holds FunctionalFAF ((FormFunctional (f,g)),v) = (f . v) * g