let A, B, C be Matrix of REAL; :: thesis: ( 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)) ; :: thesis: 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; :: thesis: verum

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)) ; :: thesis: 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; :: thesis: verum