theorem HTh8: :: ZMODLAT1:55

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