reconsider z9 = 0 as Element of REAL+ by ARYTM_2:20;
A1: x in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def 5;
per cases ( x = 0 or ( x in REAL+ & x <> 0 ) or x in [:{0},REAL+:] ) by A1, XBOOLE_0:def 3;
suppose A2: x = 0 ; :: thesis: ex b1 being Element of REAL st + (x,b1) = 0
then reconsider x9 = x as Element of REAL+ by ARYTM_2:20;
take x ; :: thesis: + (x,x) = 0
x9 + x9 = 0 by A2, ARYTM_2:def 8;
hence + (x,x) = 0 by Def1, Lm3; :: thesis: verum
end;
suppose that A3: x in REAL+ and
A4: x <> 0 ; :: thesis: ex b1 being Element of REAL st + (x,b1) = 0
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: + (x,y) = 0
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: verum
end;
suppose A8: x in [:{0},REAL+:] ; :: thesis: ex b1 being Element of REAL st + (x,b1) = 0
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: + (x,y) = 0
now :: thesis: ( ( x in REAL+ & y in REAL+ & ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & 0 = x9 + y9 ) ) or ( x in REAL+ & y in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & 0 = x9 - y9 ) ) or ( y in REAL+ & x in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & 0 = y9 - x9 ) ) 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+:] ) & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & 0 = [0,(y9 + x9)] ) ) )
per cases ( ( x in REAL+ & y in REAL+ ) or ( x in REAL+ & y in [:{0},REAL+:] ) or ( 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+:] ) ) ) ;
case ( x in REAL+ & y in REAL+ ) ; :: thesis: ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & 0 = x9 + y9 )
hence ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & 0 = x9 + y9 ) by A8, Th5, XBOOLE_0:3; :: thesis: verum
end;
case ( x in REAL+ & y in [:{0},REAL+:] ) ; :: thesis: ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & 0 = x9 - y9 )
hence ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & 0 = x9 - y9 ) by A10, Th5, XBOOLE_0:3; :: thesis: verum
end;
case ( y in REAL+ & x in [:{0},REAL+:] ) ; :: thesis: ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & 0 = y9 - x9 )
reconsider x9 = b, y9 = y as Element of REAL+ by A10;
take x9 = x9; :: thesis: ex y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & 0 = y9 - x9 )
take y9 = y9; :: thesis: ( x = [0,x9] & y = y9 & 0 = y9 - x9 )
thus x = [0,x9] by A9, A11, TARSKI:def 1; :: thesis: ( y = y9 & 0 = y9 - x9 )
thus y = y9 ; :: thesis: 0 = y9 - x9
thus 0 = y9 - x9 by ARYTM_1:18; :: thesis: verum
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: ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & 0 = [0,(y9 + x9)] )
hence ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & 0 = [0,(y9 + x9)] ) by A8, A10; :: thesis: verum
end;
end;
end;
hence + (x,y) = 0 by Def1, Lm3; :: thesis: verum
end;
end;