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