theorem :: MATRIXC1:17
for a being Element of COMPLEX
for M being Matrix of COMPLEX holds (M * a) *' = (a *') * (M *') by Th4;