theorem Th24: :: BILINEAR:24

for K being non empty multMagma
for V, W being non empty ModuleStr over K
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