let A, B, C be Matrix of REAL; ( len C = len A & width C = width A & ( for i, j being Nat st [i,j] in Indices A holds
C * (i,j) = (A * (i,j)) + (B * (i,j)) ) implies C = A + B )
assume that
A1:
( len C = len A & width C = width A )
and
A2:
for i, j being Nat st [i,j] in Indices A holds
C * (i,j) = (A * (i,j)) + (B * (i,j))
; C = A + B
set B2 = MXR2MXF B;
set A2 = MXR2MXF A;
set D = MXR2MXF C;
for i, j being Nat st [i,j] in Indices (MXR2MXF A) holds
(MXR2MXF C) * (i,j) = ((MXR2MXF A) * (i,j)) + ((MXR2MXF B) * (i,j))
by A2;
hence
C = A + B
by A1, MATRIX_3:def 3; verum