reconsider z9 = 0 as Element of REAL+ by ARYTM_2:20;
A1: x in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def 5;

per cases by A1, XBOOLE_0:def 3;

suppose A2: x = 0 ; :: thesis:

then reconsider x9 = x as Element of REAL+ by ARYTM_2:20;
take x ; :: thesis:
x9 + x9 = 0 by A2, ARYTM_2:def 8;
hence + (x,x) = 0 by Def1, Lm3; :: thesis:

end;

suppose that A3: x in REAL+ and
A4: x <> 0 ; :: thesis:

A5: [0,x] <> [0,0] by A4, XTUPLE_0:1;
0 in {0} by TARSKI:def 1;
then A6: [0,x] in [:{0},REAL+:] by A3, ZFMISC_1:87;
then [0,x] in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def 3;
then reconsider y = [0,x] as Element of REAL by A5, ZFMISC_1:56;
reconsider x9 = x as Element of REAL+ by A3;
A7: x9 <=' x9 ;
take y ; :: thesis:
z9 + x9 = x9 by ARYTM_2:def 8;
then z9 = x9 -' x9 by A7, ARYTM_1:def 1;
then 0 = x9 - x9 by A7, ARYTM_1:def 2;
hence + (x,y) = 0 by A6, Def1, Lm3; :: thesis:

end;

suppose A8: x in [:{0},REAL+:] ; :: thesis:

then consider a, b being object such that
A9: a in {0} and
A10: b in REAL+ and
A11: x = [a,b] by ZFMISC_1:84;
reconsider y = b as Element of REAL by A10, Th1;
take y ; :: thesis:

case ( x in REAL+ & y in REAL+ ) ; :: thesis:

hence ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & 0 = x9 + y9 ) by A8, Th5, XBOOLE_0:3; :: thesis:

end;

case ( x in REAL+ & y in [:{0},REAL+:] ) ; :: thesis:

hence ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & 0 = x9 - y9 ) by A10, Th5, XBOOLE_0:3; :: thesis:

end;

case ( y in REAL+ & x in [:{0},REAL+:] ) ; :: thesis:

reconsider x9 = b, y9 = y as Element of REAL+ by A10;
take x9 = x9; :: thesis:
take y9 = y9; :: thesis:
thus x = [0,x9] by A9, A11, TARSKI:def 1; :: thesis:
thus y = y9 ; :: thesis:
thus 0 = y9 - x9 by ARYTM_1:18; :: thesis:

end;

case ( ( 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:

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

end;

end;

end;

hence + (x,y) = 0 by Def1, Lm3; :: thesis:

end;

end;