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 Th2;
assume A2: z <> 0. F_Complex ; :: thesis: (- z) " = - (z ")
then A3: z1 " = z " by Th5;
- z <> 0. F_Complex by A2, VECTSP_1:28;
hence (- z) " = (- z1) " by A1, Th5
.= - (z1 ") by XCMPLX_1:222
.= - (z ") by A3, Th2 ;
:: thesis: verum