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 Element of 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 Element of NAT st [i,j] in Indices A holds
C * i,j = (A * i,j) - (B * i,j) ) ) ; :: thesis: C = A - B
A2: ( len (- B) = len B & width (- B) = width B ) by MATRIX_3:def 2;
A3: 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) )
assume A4: [i,j] in Indices A ; :: thesis: C * i,j = (A * i,j) + ((- B) * i,j)
reconsider i0 = i, j0 = j as Element of NAT by ORDINAL1:def 13;
thus C * i,j = (A * i0,j0) - (B * i0,j0) by A1, A4
.= (A * i0,j0) + (- (B * i0,j0))
.= (A * i,j) + ((- B) * i,j) by A3, A4, Th10 ; :: thesis: verum

end;

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