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

A7: now :: thesis: for i, j being Nat st [i,j] in Indices ((M1 + M2) *') holds
((M1 + M2) *') * (i,j) = ((M1 *') + (M2 *')) * (i,j)

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, Th6
.= ((M1 * (i,j)) *') + ((M2 * (i,j)) *') by COMPLEX1:32
.= ((M1 *') * (i,j)) + ((M2 * (i,j)) *') by A16, Def1
.= ((M1 *') * (i,j)) + ((M2 *') * (i,j)) by A17, Def1
.= ((M1 *') + (M2 *')) * (i,j) by A14, Th6 ;
:: thesis: verum

end;

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