let z be Element of F_Complex ; :: thesis: ( z <> 0. F_Complex implies (- z) " = - (z " ) )
reconsider z1 = z as Element of COMPLEX by Def1;
assume A1: z <> 0. F_Complex ; :: thesis: (- z) " = - (z " )
then A2: z1 " = z " by Th7;
A3: - z <> 0. F_Complex by A1, VECTSP_1:86;
- z = - z1 by Th4;
hence (- z) " = (- z1) " by A3, Th7
.= - (z1 " ) by XCMPLX_1:224
.= - (z " ) by A2, Th4 ;
:: thesis: verum