let A, B, C be Matrix of REAL ; :: thesis: ( len A = len B & width A = width B & 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 A1: ( len A = len B & width A = width B & 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) ) ) ; :: thesis: C = A + B
set D = MXR2MXF C;
set A2 = MXR2MXF A;
set B2 = MXR2MXF B;
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 A1;
hence C = A + B by A1, MATRIX_3:def 3; :: thesis: verum