theorem Th9: :: BILINEAR:9

for K being non empty 1-sorted
for V, W being non empty ModuleStr over K
for f being Form of V,W
for w being Vector of W holds
( dom (FunctionalSAF (f,w)) = the carrier of V & rng (FunctionalSAF (f,w)) c= the carrier of K & ( for v being Vector of V holds (FunctionalSAF (f,w)) . v = f . (v,w) ) )