let M1, M2 be Matrix of COMPLEX ; :: thesis: ( len M1 = len M2 & width M1 = width M2 implies (M1 - M2) *' = (M1 *' ) - (M2 *' ) )
assume that
A1: len M1 = len M2 and
A2: width M1 = width M2 ; :: thesis: (M1 - M2) *' = (M1 *' ) - (M2 *' )
A3: len ((M1 - M2) *' ) = len (M1 - M2) by Def1;
A4: width ((M1 - M2) *' ) = width (M1 - M2) by Def1;
A5: width (M1 - M2) = width M1 by Th13;
A6: width (M1 *' ) = width M1 by Def1;
A7: len (M1 *' ) = len M1 by Def1;
A8: width (M2 *' ) = width M2 by Def1;
A9: len (M1 - M2) = len M1 by Th13;
A10: len (M2 *' ) = len M2 by Def1;

A11: now

let i, j be Nat; :: thesis: ( [i,j] in Indices ((M1 - M2) *' ) implies ((M1 - M2) *' ) * i,j = ((M1 *' ) - (M2 *' )) * i,j )
assume A12: [i,j] in Indices ((M1 - M2) *' ) ; :: thesis: ((M1 - M2) *' ) * i,j = ((M1 *' ) - (M2 *' )) * i,j
then A13: 1 <= j by Th1;
A14: 1 <= i by A12, Th1;
A15: j <= width (M1 - M2) by A4, A12, Th1;
then A16: j <= width (M1 *' ) by A5, Def1;
A17: i <= len (M1 - M2) by A3, A12, Th1;
then i <= len (M1 *' ) by A9, Def1;
then A18: [i,j] in Indices (M1 *' ) by A13, A14, A16, Th1;
A19: 1 <= i by A12, Th1;
then A20: [i,j] in Indices M1 by A9, A5, A17, A13, A15, Th1;
A21: [i,j] in Indices M2 by A1, A2, A9, A5, A19, A17, A13, A15, Th1;
[i,j] in Indices (M1 - M2) by A19, A17, A13, A15, Th1;
then ((M1 - M2) *' ) * i,j = ((M1 - M2) * i,j) *' by Def1;
hence ((M1 - M2) *' ) * i,j = ((M1 * i,j) - (M2 * i,j)) *' by A1, A2, A20, Th14
.= ((M1 * i,j) *' ) - ((M2 * i,j) *' ) by COMPLEX1:120
.= ((M1 *' ) * i,j) - ((M2 * i,j) *' ) by A20, Def1
.= ((M1 *' ) * i,j) - ((M2 *' ) * i,j) by A21, Def1
.= ((M1 *' ) - (M2 *' )) * i,j by A1, A2, A7, A10, A6, A8, A18, Th14 ;
:: thesis: verum

end;

A22: width (M1 *' ) = width M1 by Def1;
A23: width ((M1 *' ) - (M2 *' )) = width (M1 *' ) by Th13;
len ((M1 *' ) - (M2 *' )) = len (M1 *' ) by Th13;
hence (M1 - M2) *' = (M1 *' ) - (M2 *' ) by A3, A7, A9, A4, A5, A23, A22, A11, MATRIX_1:21; :: thesis: verum