theorem :: ZMATRLIN:64

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