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

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