let x, y, z be Element of REAL ; ( + (x,y) = 0 & + (x,z) = 0 implies y = z )
assume that
A1:
+ (x,y) = 0
and
A2:
+ (x,z) = 0
; 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+:] ) ) )
;
suppose that A3:
x in REAL+
and A4:
y in REAL+
and A5:
z in [:{0},REAL+:]
;
y = zA6:
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;
verum end; suppose that A11:
x in REAL+
and A12:
z in REAL+
and A13:
y in [:{0},REAL+:]
;
y = zA14:
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;
verum end; suppose that A19:
x in REAL+
and A20:
y in [:{0},REAL+:]
and A21:
z in [:{0},REAL+:]
;
y = zconsider 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;
verum end; suppose that A28:
z in REAL+
and A29:
y in REAL+
and A30:
x in [:{0},REAL+:]
;
y = zconsider 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;
verum end;