theorem Th25: :: MATRIXR1:25

for A, B being Matrix of REAL holds
( len (A + B) = len A & width (A + B) = width A & ( for i, j being Nat st [i,j] in Indices A holds
(A + B) * (i,j) = (A * (i,j)) + (B * (i,j)) ) )