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 Element of 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 Element of 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 Element of 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 Element of NAT st [i,j] in Indices A holds
(A - B) * i,j = (A * i,j) - (B * i,j)
thus for i, j being Element of NAT st [i,j] in Indices A holds
(A - B) * i,j = (A * i,j) - (B * i,j) by A1, MATRIX10:3; :: thesis: verum