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 that
A1: len M1 = len M2 and
A2: width M1 = width M2 and
A3: [i,j] in Indices M1 ; :: thesis: (M1 - M2) * i,j = (M1 * i,j) - (M2 * i,j)
A4: ( 1 <= j & j <= width M2 ) by A2, A3, MATRIXC1:1;
( 1 <= i & i <= len M2 ) by A1, A3, MATRIXC1:1;
then A5: [i,j] in Indices (MXR2MXF M2) by A4, 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 A3, MATRIX_3:def 3
.= ((MXR2MXF M1) * i,j) + (- ((MXR2MXF M2) * i,j)) by A5, MATRIX_3:def 2 ;
hence (M1 - M2) * i,j = (M1 * i,j) - (M2 * i,j) by VECTSP_1:def 15; :: thesis: verum