let i, j be Nat; 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; ( 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
; (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; verum