let z be Element of F_Complex ; :: thesis: (- z) *' = - (z *' )
reconsider z' = z as Element of COMPLEX by Def1;
- z = - z' by Th4;
hence (- z) *' = - (z' *' ) by COMPLEX1:119
.= - (z *' ) by Th4 ;
:: thesis: verum