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 x1', x2', y1', y2' being Element of REAL such that
A9: z = [*x1',x2'*] and
A10: c2 = [*y1',y2'*] and
A11: 0 = [*(+ x1',y1'),(+ x2',y2')*] by A5, Def4;
A12: x1 = x1' by A6, A9, ARYTM_0:12;
A13: x2 = x2' by A6, A9, ARYTM_0:12;
A14: + x1,y1 = 0 by A8, Lm1, ARYTM_0:12;
A15: + x1,y1' = 0 by A11, A12, Lm1, ARYTM_0:12;
A16: y1 = y1' by A14, A15, Lm2;
A17: + x2,y2 = 0 by A8, Lm1, ARYTM_0:12;
A18: + x2,y2' = 0 by A11, A13, Lm1, ARYTM_0:12;
thus c1 = c2 by A7, A10, A16, A17, A18, Lm2; :: thesis: verum