let y, z be Element of REAL ; ( + (x,y) = 0 & + (x,z) = 0 implies y = z )
assume that
A12:
+ (x,y) = 0
and
A13:
+ (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 A14:
x in REAL+
and A15:
y in REAL+
and A16:
z in [:{0},REAL+:]
;
y = zconsider x99,
y99 being
Element of
REAL+ such that A17:
x = x99
and A18:
(
z = [0,y99] &
0 = x99 - y99 )
by A13, A14, A16, Def1;
ex
x9,
y9 being
Element of
REAL+ st
(
x = x9 &
y = y9 &
0 = x9 + y9 )
by A12, A14, A15, Def1;
then A19:
x99 = 0
by A17, ARYTM_2:5;
[0,0] in {[0,0]}
by TARSKI:def 1;
then A20:
not
[0,0] in REAL
by XBOOLE_0:def 5;
z in REAL
;
hence
y = z
by A18, A19, A20, ARYTM_1:19;
verum end; suppose that A21:
x in REAL+
and A22:
z in REAL+
and A23:
y in [:{0},REAL+:]
;
y = zconsider x99,
y9 being
Element of
REAL+ such that A24:
x = x99
and A25:
(
y = [0,y9] &
0 = x99 - y9 )
by A12, A21, A23, Def1;
ex
x9,
z9 being
Element of
REAL+ st
(
x = x9 &
z = z9 &
0 = x9 + z9 )
by A13, A21, A22, Def1;
then A26:
x99 = 0
by A24, ARYTM_2:5;
[0,0] in {[0,0]}
by TARSKI:def 1;
then A27:
not
[0,0] in REAL
by XBOOLE_0:def 5;
y in REAL
;
hence
y = z
by A25, A26, A27, ARYTM_1:19;
verum end; suppose that A28:
x in REAL+
and A29:
y in [:{0},REAL+:]
and A30:
z in [:{0},REAL+:]
;
y = zconsider x99,
z9 being
Element of
REAL+ such that A31:
x = x99
and A32:
z = [0,z9]
and A33:
0 = x99 - z9
by A13, A28, A30, Def1;
consider x9,
y9 being
Element of
REAL+ such that A34:
x = x9
and A35:
y = [0,y9]
and A36:
0 = x9 - y9
by A12, A28, A29, Def1;
y9 =
x9
by A36, Th6
.=
z9
by A34, A31, A33, Th6
;
hence
y = z
by A35, A32;
verum end; suppose that A37:
z in REAL+
and A38:
y in REAL+
and A39:
x in [:{0},REAL+:]
;
y = zconsider x99,
z9 being
Element of
REAL+ such that A40:
x = [0,x99]
and A41:
z = z9
and A42:
0 = z9 - x99
by A13, A37, A39, Def1;
consider x9,
y9 being
Element of
REAL+ such that A43:
x = [0,x9]
and A44:
y = y9
and A45:
0 = y9 - x9
by A12, A38, A39, Def1;
x9 = x99
by A43, A40, XTUPLE_0:1;
then z9 =
x9
by A42, Th6
.=
y9
by A45, Th6
;
hence
y = z
by A44, A41;
verum end;