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