theorem Th14: :: BILINEAR:14

for K being non empty doubleLoopStr
for V, W being non empty ModuleStr over K
for f being Form of V,W
for a being Element of K
for w being Vector of W holds FunctionalSAF ((a * f),w) = a * (FunctionalSAF (f,w))