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