theorem BLTh8: :: ZMATRLIN:67

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