theorem BLTh15: :: ZMATRLIN:74

for V, W being non empty ModuleStr over INT.Ring
for f being Form of V,W
for a being Element of INT.Ring
for v being Vector of V holds FunctionalFAF ((a * f),v) = a * (FunctionalFAF (f,v))