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 that
A1: ( len A = len B & width A = width B ) and
A2: ( len C = len A & width C = width A ) and
A3: 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
A4: Indices B = Indices A by A1, MATRIX_4:55;
for i, j being Nat st [i,j] in Indices A holds
C * (i,j) = (A * (i,j)) + ((- B) * (i,j))

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices A implies C * (i,j) = (A * (i,j)) + ((- B) * (i,j)) )
reconsider i0 = i, j0 = j as Nat ;
assume A5: [i,j] in Indices A ; :: thesis: C * (i,j) = (A * (i,j)) + ((- B) * (i,j))
hence C * (i,j) = (A * (i0,j0)) - (B * (i0,j0)) by A3
.= (A * (i0,j0)) + (- (B * (i0,j0)))
.= (A * (i,j)) + ((- B) * (i,j)) by A4, A5, Th10 ;
:: thesis: verum

end;

then C = A + (- B) by A2, MATRIXR1:26;
hence C = A - B by MATRIX_4:def 1; :: thesis: verum