let A, B be Matrix of REAL; :: thesis: ( len A = len B & width A = width B implies ( len (A - B) = len A & width (A - B) = width A & ( for i, j being Nat st [i,j] in Indices A holds
(A - B) * (i,j) = (A * (i,j)) - (B * (i,j)) ) ) )
assume A1: ( len A = len B & width A = width B ) ; :: thesis: ( len (A - B) = len A & width (A - B) = width A & ( for i, j being Nat st [i,j] in Indices A holds
(A - B) * (i,j) = (A * (i,j)) - (B * (i,j)) ) )
thus len (A - B) = len (MXF2MXR ((MXR2MXF A) + (- (MXR2MXF B)))) by MATRIX_4:def 1
.= len A by MATRIX_3:def 3 ; :: thesis: ( width (A - B) = width A & ( for i, j being Nat st [i,j] in Indices A holds
(A - B) * (i,j) = (A * (i,j)) - (B * (i,j)) ) )
thus width (A - B) = width (MXF2MXR ((MXR2MXF A) + (- (MXR2MXF B)))) by MATRIX_4:def 1
.= width A by MATRIX_3:def 3 ; :: thesis: for i, j being Nat st [i,j] in Indices A holds
(A - B) * (i,j) = (A * (i,j)) - (B * (i,j))
thus for i, j being Nat st [i,j] in Indices A holds
(A - B) * (i,j) = (A * (i,j)) - (B * (i,j)) by A1, MATRIX10:3; :: thesis: verum