theorem :: MATRIXR1:32

for A being Matrix of REAL holds 1 * A = A