let i, j be Nat; :: thesis: for M1, M2 being Matrix of COMPLEX 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 COMPLEX ; :: 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 Th1;
then A2: [i,j] in Indices M2 by Th1;
A3: COMPLEX2Field (M1 - M2) = COMPLEX2Field (Field2COMPLEX ((COMPLEX2Field M1) - (COMPLEX2Field M2))) by MATRIX_5:def 5
.= (COMPLEX2Field M1) - (COMPLEX2Field M2) by MATRIX_5:6 ;
A4: [i,j] in Indices (COMPLEX2Field M1) by A1, MATRIX_5:def 1;
A5: [i,j] in Indices (COMPLEX2Field M2) by A2, MATRIX_5:def 1;
set m = COMPLEX2Field (M1 - M2);
reconsider m' = COMPLEX2Field (M1 - M2) as Matrix of COMPLEX by COMPLFLD:def 1;
reconsider m1 = COMPLEX2Field M1 as Matrix of COMPLEX by COMPLFLD:def 1;
reconsider m2 = COMPLEX2Field M2 as Matrix of COMPLEX by COMPLFLD:def 1;
A6: M1 * i,j = m1 * i,j by MATRIX_5:def 1
.= (COMPLEX2Field M1) * i,j by COMPLFLD:def 1 ;
M2 * i,j = m2 * i,j by MATRIX_5:def 1
.= (COMPLEX2Field M2) * i,j by COMPLFLD:def 1 ;
then A7: - (M2 * i,j) = - ((COMPLEX2Field M2) * i,j) by COMPLFLD:4;
(M1 - M2) * i,j = m' * i,j by MATRIX_5:def 1
.= (COMPLEX2Field (M1 - M2)) * i,j by COMPLFLD:def 1
.= ((COMPLEX2Field M1) + (- (COMPLEX2Field M2))) * i,j by A3, MATRIX_4:def 1
.= ((COMPLEX2Field M1) * i,j) + ((- (COMPLEX2Field M2)) * i,j) by A4, MATRIX_3:def 3
.= ((COMPLEX2Field M1) * i,j) + (- ((COMPLEX2Field M2) * i,j)) by A5, MATRIX_3:def 2 ;
hence (M1 - M2) * i,j = (M1 * i,j) - (M2 * i,j) by A6, A7; :: thesis: verum