theorem :: ZMATRLIN:65

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 * (b * f)