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