let y, z be Element of REAL ; :: thesis:
assume that
A12: + (x,y) = 0 and
A13: + (x,z) = 0 ; :: thesis:

suppose ( x in REAL+ & y in REAL+ & z in REAL+ ) ; :: thesis:

then ( ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & 0 = x9 + y9 ) & ex x9, y9 being Element of REAL+ st
( x = x9 & z = y9 & 0 = x9 + y9 ) ) by A12, A13, Def1;
hence y = z by ARYTM_2:11; :: thesis:

end;

suppose that A14: x in REAL+ and
A15: y in REAL+ and
A16: z in [:{0},REAL+:] ; :: thesis:

consider 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; :: thesis:

end;

suppose that A21: x in REAL+ and
A22: z in REAL+ and
A23: y in [:{0},REAL+:] ; :: thesis:

consider 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; :: thesis:

end;

suppose that A28: x in REAL+ and
A29: y in [:{0},REAL+:] and
A30: z in [:{0},REAL+:] ; :: thesis:

consider 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; :: thesis:

end;

suppose that A37: z in REAL+ and
A38: y in REAL+ and
A39: x in [:{0},REAL+:] ; :: thesis:

consider 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; :: thesis:

end;

suppose ( ( 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+:] ) ) ; :: thesis:

then ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & 0 = [0,(x9 + y9)] ) by A12, Def1;
hence y = z ; :: thesis:

end;

suppose ( ( 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+:] ) ) ; :: thesis:

then ex x9, z9 being Element of REAL+ st
( x = [0,x9] & z = [0,z9] & 0 = [0,(x9 + z9)] ) by A13, Def1;
hence y = z ; :: thesis:

end;

end;