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