let i, j be Nat; :: thesis: for M1, M2 being Matrix of REAL st len M1 = len M2 & width M1 = width M2 & [i,j] in Indices M1 holds
(M1 - M2) * i,j = (M1 * i,j) - (M2 * i,j)
let M1, M2 be Matrix of REAL ; :: thesis: ( len M1 = len M2 & width M1 = width M2 & [i,j] in Indices M1 implies (M1 - M2) * i,j = (M1 * i,j) - (M2 * i,j) )
assume A1: ( len M1 = len M2 & width M1 = width M2 & [i,j] in Indices M1 ) ; :: thesis: (M1 - M2) * i,j = (M1 * i,j) - (M2 * i,j)
then ( 1 <= i & i <= len M2 & 1 <= j & j <= width M2 ) by MATRIXC1:1;
then A2: [i,j] in Indices (MXR2MXF M2) by MATRIXC1:1;
(M1 - M2) * i,j = ((MXR2MXF M1) + (- (MXR2MXF M2))) * i,j by MATRIX_4:def 1, VECTSP_1:def 15
.= ((MXR2MXF M1) * i,j) + ((- (MXR2MXF M2)) * i,j) by A1, MATRIX_3:def 3
.= ((MXR2MXF M1) * i,j) + (- ((MXR2MXF M2) * i,j)) by A2, MATRIX_3:def 2 ;
hence (M1 - M2) * i,j = (M1 * i,j) - (M2 * i,j) by VECTSP_1:def 15; :: thesis: verum