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