theorem Th12: :: MATRIXR2:12

for a, b being Real
for A being Matrix of REAL holds (a + b) * A = (a * A) + (b * A)