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 by Th6;
A4: width ((M1 + M2) *' ) = width (M1 + M2) by Def1;
A5: width (M1 + M2) = width M1 by Th6;
A6: len ((M1 + M2) *' ) = len (M1 + M2) by Def1;

A7: now

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

end;

A18: width (M1 *' ) = width M1 by Def1;
A19: width ((M1 *' ) + (M2 *' )) = width (M1 *' ) by Th6;
A20: len ((M1 *' ) + (M2 *' )) = len (M1 *' ) by Th6;
len (M1 *' ) = len M1 by Def1;
hence (M1 + M2) *' = (M1 *' ) + (M2 *' ) by A6, A3, A20, A4, A5, A19, A18, A7, MATRIX_1:21; :: thesis: verum