theorem Th29: :: MATRIXR1:29

for a being Real
for A being Matrix of REAL
for i2, j2 being Nat st [i2,j2] in Indices A holds
(a * A) * (i2,j2) = a * (A * (i2,j2))