theorem :: ZMATRLIN:63

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