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

(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