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