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