theorem Th25: :: BILINEAR:25

for K being non empty commutative multMagma
for V, W being non empty ModuleStr over K
for f being Functional of V
for g being Functional of W
for w being Vector of W holds FunctionalSAF ((FormFunctional (f,g)),w) = (g . w) * f