theorem :: MATRIXR1:34

for A being Matrix of REAL holds (A + A) + A = 3 * A