let M be Matrix of COMPLEX; :: thesis: (- M) *' = - (M *')
(- M) *' = ((- 1) * M) *' by Th11
.= ((- 1r) *') * (M *') by Th5, COMPLEX1:def 4
.= (- 1) * (M *') by COMPLEX1:30, COMPLEX1:33, COMPLEX1:def 4
.= - (M *') by Th11 ;
hence (- M) *' = - (M *') ; :: thesis: verum