let c1, c2 be Complex; :: thesis: ( z + c1 = 0 & z + c2 = 0 implies c1 = c2 )
assume that
A2: z + c1 = 0 and
A3: z + c2 = 0 ; :: thesis: c1 = c2
consider x1, x2, y1, y2 being Element of REAL such that
A4: z = [*x1,x2*] and
A5: c1 = [*y1,y2*] and
A6: 0 = [*(+ (x1,y1)),(+ (x2,y2))*] by A2, Def3;
consider x19, x29, y19, y29 being Element of REAL such that
A7: z = [*x19,x29*] and
A8: c2 = [*y19,y29*] and
A9: 0 = [*(+ (x19,y19)),(+ (x29,y29))*] by A3, Def3;
A10: x1 = x19 by A4, A7, ARYTM_0:10;
A11: x2 = x29 by A4, A7, ARYTM_0:10;
0 in NAT ;
then reconsider zz = 0 as Element of REAL by NUMBERS:19;
Lm3: 0 = [*zz,zz*] by ARYTM_0:def 5;
A12: + (x1,y1) = 0 by A6, Lm3, ARYTM_0:10;
+ (x1,y19) = 0 by A9, A10, Lm3, ARYTM_0:10;
then A13: y1 = y19 by A12, Lm4;
A14: + (x2,y2) = 0 by A6, Lm3, ARYTM_0:10;
+ (x2,y29) = 0 by A9, A11, Lm3, ARYTM_0:10;
hence c1 = c2 by A5, A8, A13, A14, Lm4; :: thesis: verum