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 5
.= ((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 5; :: thesis: verum