let x, y, z be Element of REAL ; :: thesis: ( + (x,y) = 0 & + (x,z) = 0 implies y = z )

assume that

A1: + (x,y) = 0 and

A2: + (x,z) = 0 ; :: thesis: y = z

assume that

A1: + (x,y) = 0 and

A2: + (x,z) = 0 ; :: thesis: y = z

per cases
( ( x in REAL+ & y in REAL+ & z in REAL+ ) or ( x in REAL+ & y in REAL+ & z in [:{0},REAL+:] ) or ( x in REAL+ & z in REAL+ & y in [:{0},REAL+:] ) or ( x in REAL+ & y in [:{0},REAL+:] & z in [:{0},REAL+:] ) or ( z in REAL+ & y in REAL+ & x in [:{0},REAL+:] ) or ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] ) & ( not y in REAL+ or not x in [:{0},REAL+:] ) ) or ( ( not x in REAL+ or not z in REAL+ ) & ( not x in REAL+ or not z in [:{0},REAL+:] ) & ( not z in REAL+ or not x in [:{0},REAL+:] ) ) )
;

end;

suppose
( x in REAL+ & y in REAL+ & z in REAL+ )
; :: thesis: y = z

then
( ex x9, y9 being Element of REAL+ st

( x = x9 & y = y9 & 0 = x9 + y9 ) & ex x9, y9 being Element of REAL+ st

( x = x9 & z = y9 & 0 = x9 + y9 ) ) by A1, A2, ARYTM_0:def 1;

hence y = z by ARYTM_2:11; :: thesis: verum

end;( x = x9 & y = y9 & 0 = x9 + y9 ) & ex x9, y9 being Element of REAL+ st

( x = x9 & z = y9 & 0 = x9 + y9 ) ) by A1, A2, ARYTM_0:def 1;

hence y = z by ARYTM_2:11; :: thesis: verum

suppose that A3:
x in REAL+
and

A4: y in REAL+ and

A5: z in [:{0},REAL+:] ; :: thesis: y = z

A4: y in REAL+ and

A5: z in [:{0},REAL+:] ; :: thesis: y = z

A6:
ex x9, y9 being Element of REAL+ st

( x = x9 & y = y9 & 0 = x9 + y9 ) by A1, A3, A4, ARYTM_0:def 1;

consider x99, y99 being Element of REAL+ such that

A7: x = x99 and

A8: ( z = [0,y99] & 0 = x99 - y99 ) by A2, A3, A5, ARYTM_0:def 1;

A9: x99 = 0 by A6, A7, ARYTM_2:5;

[{},{}] in {[{},{}]} by TARSKI:def 1;

then A10: not [{},{}] in REAL by NUMBERS:def 1, XBOOLE_0:def 5;

z in REAL ;

hence y = z by A8, A9, A10, ARYTM_1:19; :: thesis: verum

end;( x = x9 & y = y9 & 0 = x9 + y9 ) by A1, A3, A4, ARYTM_0:def 1;

consider x99, y99 being Element of REAL+ such that

A7: x = x99 and

A8: ( z = [0,y99] & 0 = x99 - y99 ) by A2, A3, A5, ARYTM_0:def 1;

A9: x99 = 0 by A6, A7, ARYTM_2:5;

[{},{}] in {[{},{}]} by TARSKI:def 1;

then A10: not [{},{}] in REAL by NUMBERS:def 1, XBOOLE_0:def 5;

z in REAL ;

hence y = z by A8, A9, A10, ARYTM_1:19; :: thesis: verum

suppose that A11:
x in REAL+
and

A12: z in REAL+ and

A13: y in [:{0},REAL+:] ; :: thesis: y = z

A12: z in REAL+ and

A13: y in [:{0},REAL+:] ; :: thesis: y = z

A14:
ex x9, z9 being Element of REAL+ st

( x = x9 & z = z9 & 0 = x9 + z9 ) by A2, A11, A12, ARYTM_0:def 1;

consider x99, y9 being Element of REAL+ such that

A15: x = x99 and

A16: ( y = [0,y9] & 0 = x99 - y9 ) by A1, A11, A13, ARYTM_0:def 1;

A17: x99 = 0 by A14, A15, ARYTM_2:5;

[0,0] in {[0,0]} by TARSKI:def 1;

then A18: not [0,0] in REAL by NUMBERS:def 1, XBOOLE_0:def 5;

y in REAL ;

hence y = z by A16, A17, A18, ARYTM_1:19; :: thesis: verum

end;( x = x9 & z = z9 & 0 = x9 + z9 ) by A2, A11, A12, ARYTM_0:def 1;

consider x99, y9 being Element of REAL+ such that

A15: x = x99 and

A16: ( y = [0,y9] & 0 = x99 - y9 ) by A1, A11, A13, ARYTM_0:def 1;

A17: x99 = 0 by A14, A15, ARYTM_2:5;

[0,0] in {[0,0]} by TARSKI:def 1;

then A18: not [0,0] in REAL by NUMBERS:def 1, XBOOLE_0:def 5;

y in REAL ;

hence y = z by A16, A17, A18, ARYTM_1:19; :: thesis: verum

suppose that A19:
x in REAL+
and

A20: y in [:{0},REAL+:] and

A21: z in [:{0},REAL+:] ; :: thesis: y = z

A20: y in [:{0},REAL+:] and

A21: z in [:{0},REAL+:] ; :: thesis: y = z

consider x9, y9 being Element of REAL+ such that

A22: x = x9 and

A23: y = [0,y9] and

A24: 0 = x9 - y9 by A1, A19, A20, ARYTM_0:def 1;

consider x99, z9 being Element of REAL+ such that

A25: x = x99 and

A26: z = [0,z9] and

A27: 0 = x99 - z9 by A2, A19, A21, ARYTM_0:def 1;

y9 = x9 by A24, ARYTM_0:6

.= z9 by A22, A25, A27, ARYTM_0:6 ;

hence y = z by A23, A26; :: thesis: verum

end;A22: x = x9 and

A23: y = [0,y9] and

A24: 0 = x9 - y9 by A1, A19, A20, ARYTM_0:def 1;

consider x99, z9 being Element of REAL+ such that

A25: x = x99 and

A26: z = [0,z9] and

A27: 0 = x99 - z9 by A2, A19, A21, ARYTM_0:def 1;

y9 = x9 by A24, ARYTM_0:6

.= z9 by A22, A25, A27, ARYTM_0:6 ;

hence y = z by A23, A26; :: thesis: verum

suppose that A28:
z in REAL+
and

A29: y in REAL+ and

A30: x in [:{0},REAL+:] ; :: thesis: y = z

A29: y in REAL+ and

A30: x in [:{0},REAL+:] ; :: thesis: y = z

consider x9, y9 being Element of REAL+ such that

A31: x = [0,x9] and

A32: y = y9 and

A33: 0 = y9 - x9 by A1, A29, A30, ARYTM_0:def 1;

consider x99, z9 being Element of REAL+ such that

A34: x = [0,x99] and

A35: z = z9 and

A36: 0 = z9 - x99 by A2, A28, A30, ARYTM_0:def 1;

x9 = x99 by A31, A34, XTUPLE_0:1;

then z9 = x9 by A36, ARYTM_0:6

.= y9 by A33, ARYTM_0:6 ;

hence y = z by A32, A35; :: thesis: verum

end;A31: x = [0,x9] and

A32: y = y9 and

A33: 0 = y9 - x9 by A1, A29, A30, ARYTM_0:def 1;

consider x99, z9 being Element of REAL+ such that

A34: x = [0,x99] and

A35: z = z9 and

A36: 0 = z9 - x99 by A2, A28, A30, ARYTM_0:def 1;

x9 = x99 by A31, A34, XTUPLE_0:1;

then z9 = x9 by A36, ARYTM_0:6

.= y9 by A33, ARYTM_0:6 ;

hence y = z by A32, A35; :: thesis: verum

suppose
( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] ) & ( not y in REAL+ or not x in [:{0},REAL+:] ) )
; :: thesis: y = z

then
ex x9, y9 being Element of REAL+ st

( x = [0,x9] & y = [0,y9] & 0 = [0,(x9 + y9)] ) by A1, ARYTM_0:def 1;

hence y = z ; :: thesis: verum

end;( x = [0,x9] & y = [0,y9] & 0 = [0,(x9 + y9)] ) by A1, ARYTM_0:def 1;

hence y = z ; :: thesis: verum

suppose
( ( not x in REAL+ or not z in REAL+ ) & ( not x in REAL+ or not z in [:{0},REAL+:] ) & ( not z in REAL+ or not x in [:{0},REAL+:] ) )
; :: thesis: y = z

then
ex x9, z9 being Element of REAL+ st

( x = [0,x9] & z = [0,z9] & 0 = [0,(x9 + z9)] ) by A2, ARYTM_0:def 1;

hence y = z ; :: thesis: verum

end;( x = [0,x9] & z = [0,z9] & 0 = [0,(x9 + z9)] ) by A2, ARYTM_0:def 1;

hence y = z ; :: thesis: verum