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