let a be Complex; :: thesis: for M being Matrix of COMPLEX holds (a * M) *' = (a *') * (M *')
let M be Matrix of COMPLEX; :: thesis: (a * M) *' = (a *') * (M *')
reconsider aa = a as Element of COMPLEX by XCMPLX_0:def 2;
A1: len (a * M) = len M by Th2;
A2: width (a * M) = width M by Th2;
A3: width M = width (M *') by Def1;
A4: len ((a * M) *') = len (a * M) by Def1;
A5: width ((a * M) *') = width (a * M) by Def1;
A6: len M = len (M *') by Def1;

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

let i, j be Nat; :: thesis: ( [i,j] in Indices ((a * M) *') implies ((a * M) *') * (i,j) = ((a *') * (M *')) * (i,j) )
assume A8: [i,j] in Indices ((a * M) *') ; :: thesis: ((a * M) *') * (i,j) = ((a *') * (M *')) * (i,j)
then A9: 1 <= i by Th1;
A10: 1 <= j by A8, Th1;
A11: j <= width (a * M) by A5, A8, Th1;
A12: i <= len (a * M) by A4, A8, Th1;
then A13: [i,j] in Indices M by A1, A2, A9, A10, A11, Th1;
A14: [i,j] in Indices (M *') by A1, A6, A2, A3, A9, A12, A10, A11, Th1;
[i,j] in Indices (a * M) by A9, A12, A10, A11, Th1;
then ((a * M) *') * (i,j) = ((a * M) * (i,j)) *' by Def1;
hence ((a * M) *') * (i,j) = (aa * (M * (i,j))) *' by A13, Th3
.= (aa *') * ((M * (i,j)) *') by COMPLEX1:35
.= (a *') * ((M *') * (i,j)) by A13, Def1
.= ((a *') * (M *')) * (i,j) by A14, Th3 ;
:: thesis: verum

end;

len ((a *') * (M *')) = len (M *') by Th2;
then len ((a *') * (M *')) = len M by Def1;
then A15: len ((a * M) *') = len ((a *') * (M *')) by A4, Th2;
width ((a *') * (M *')) = width (M *') by Th2;
then width ((a *') * (M *')) = width M by Def1;
hence (a * M) *' = (a *') * (M *') by A15, A5, A7, Th2, MATRIX_0:21; :: thesis: verum