theorem BLTh9: :: ZMATRLIN:68

for V, W being non empty ModuleStr over INT.Ring
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 INT.Ring & ( for v being Vector of V holds (FunctionalSAF (f,w)) . v = f . (v,w) ) )