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 A5:
x in REAL+
and A6:
y in REAL+
and A7:
z in [:{0 },REAL+ :]
;
y = zA8:
ex
x9,
y9 being
Element of
REAL+ st
(
x = x9 &
y = y9 &
0 = x9 + y9 )
by A1, A5, A6, ARYTM_0:def 2;
consider x99,
y99 being
Element of
REAL+ such that A9:
x = x99
and A10:
(
z = [0 ,y99] &
0 = x99 - y99 )
by A2, A5, A7, ARYTM_0:def 2;
A11:
x99 = 0
by A8, A9, ARYTM_2:6;
A12:
[{} ,{} ] in {[{} ,{} ]}
by TARSKI:def 1;
A13:
not
[{} ,{} ] in REAL
by A12, NUMBERS:def 1, XBOOLE_0:def 5;
A14:
z in REAL
;
thus
y = z
by A10, A11, A13, A14, ARYTM_1:19;
verum end; suppose that A15:
x in REAL+
and A16:
z in REAL+
and A17:
y in [:{0 },REAL+ :]
;
y = zA18:
ex
x9,
z9 being
Element of
REAL+ st
(
x = x9 &
z = z9 &
0 = x9 + z9 )
by A2, A15, A16, ARYTM_0:def 2;
consider x99,
y9 being
Element of
REAL+ such that A19:
x = x99
and A20:
(
y = [0 ,y9] &
0 = x99 - y9 )
by A1, A15, A17, ARYTM_0:def 2;
A21:
x99 = 0
by A18, A19, ARYTM_2:6;
A22:
[0 ,0 ] in {[0 ,0 ]}
by TARSKI:def 1;
A23:
not
[0 ,0 ] in REAL
by A22, NUMBERS:def 1, XBOOLE_0:def 5;
A24:
y in REAL
;
thus
y = z
by A20, A21, A23, A24, ARYTM_1:19;
verum end; suppose that A25:
x in REAL+
and A26:
y in [:{0 },REAL+ :]
and A27:
z in [:{0 },REAL+ :]
;
y = zconsider x9,
y9 being
Element of
REAL+ such that A28:
x = x9
and A29:
y = [0 ,y9]
and A30:
0 = x9 - y9
by A1, A25, A26, ARYTM_0:def 2;
consider x99,
z9 being
Element of
REAL+ such that A31:
x = x99
and A32:
z = [0 ,z9]
and A33:
0 = x99 - z9
by A2, A25, A27, ARYTM_0:def 2;
A34:
y9 =
x9
by A30, ARYTM_0:6
.=
z9
by A28, A31, A33, ARYTM_0:6
;
thus
y = z
by A29, A32, A34;
verum end; suppose that A35:
z in REAL+
and A36:
y in REAL+
and A37:
x in [:{0 },REAL+ :]
;
y = zconsider x9,
y9 being
Element of
REAL+ such that A38:
x = [0 ,x9]
and A39:
y = y9
and A40:
0 = y9 - x9
by A1, A36, A37, ARYTM_0:def 2;
consider x99,
z9 being
Element of
REAL+ such that A41:
x = [0 ,x99]
and A42:
z = z9
and A43:
0 = z9 - x99
by A2, A35, A37, ARYTM_0:def 2;
A44:
x9 = x99
by A38, A41, ZFMISC_1:33;
A45:
z9 =
x9
by A43, A44, ARYTM_0:6
.=
y9
by A40, ARYTM_0:6
;
thus
y = z
by A39, A42, A45;
verum end;