theorem HTh9: :: ZMODLAT1:56

for V, W being non empty ModuleStr over INT.Ring
for f being FrForm of V,W
for w being Vector of W holds
( dom (FrFunctionalSAF (f,w)) = the carrier of V & rng (FrFunctionalSAF (f,w)) c= the carrier of F_Real & ( for v being Vector of V holds (FrFunctionalSAF (f,w)) . v = f . (v,w) ) )