let c1, c2 be complex number ; :: thesis: ( z + c1 = 0 & z + c2 = 0 implies c1 = c2 )
assume that
A4: z + c1 = 0 and
A5: z + c2 = 0 ; :: thesis: c1 = c2
consider x1, x2, y1, y2 being Element of REAL such that
A6: z = [*x1,x2*] and
A7: c1 = [*y1,y2*] and
A8: 0 = [*(+ x1,y1),(+ x2,y2)*] by A4, Def4;
consider x19, x29, y19, y29 being Element of REAL such that
A9: z = [*x19,x29*] and
A10: c2 = [*y19,y29*] and
A11: 0 = [*(+ x19,y19),(+ x29,y29)*] by A5, Def4;
A12: x1 = x19 by A6, A9, ARYTM_0:12;
A13: x2 = x29 by A6, A9, ARYTM_0:12;
A14: + x1,y1 = 0 by A8, Lm1, ARYTM_0:12;
+ x1,y19 = 0 by A11, A12, Lm1, ARYTM_0:12;
then A16: y1 = y19 by A14, Lm2;
A17: + x2,y2 = 0 by A8, Lm1, ARYTM_0:12;
+ x2,y29 = 0 by A11, A13, Lm1, ARYTM_0:12;
hence c1 = c2 by A7, A10, A16, A17, Lm2; :: thesis: verum