let x1 be Element of F_Complex; :: thesis: for x2 being Complex st x1 = x2 holds
- x1 = - x2
let x2 be Complex; :: thesis: ( x1 = x2 implies - x1 = - x2 )
assume A1: x1 = x2 ; :: thesis: - x1 = - x2
reconsider x2 = x2 as Element of COMPLEX by XCMPLX_0:def 2;
- x2 in COMPLEX by XCMPLX_0:def 2;
then reconsider x9 = - x2 as Element of F_Complex by Def1;
x1 + x9 = 0. F_Complex by A1, Def1;
hence - x1 = - x2 by RLVECT_1:def 10; :: thesis: verum