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