let a be real number ; :: thesis: for x' being Element of REAL+ st x' = a holds
0' - x' = - a
let xx be Element of REAL+ ; :: thesis: ( xx = a implies 0' - xx = - a )
assume A1: xx = a ; :: thesis: 0' - xx = - a

per cases ( xx = 0 or xx <> 0 ) ;

suppose xx = 0 ; :: thesis: 0' - xx = - a

hence 0' - xx = - a by A1, ARYTM_1:18; :: thesis: verum

end;

suppose A2: xx <> 0 ; :: thesis: 0' - xx = - a

set b = 0' - xx;
A3: 0' <=' xx by ARYTM_1:6;
then not xx <=' 0' by A2, ARYTM_1:4;
then A4: 0' - xx = [{} ,(xx -' 0')] by ARYTM_1:def 2;

now

assume 0' - xx = [0 ,0 ] ; :: thesis: contradiction
then xx -' 0' = 0 by A4, ZFMISC_1:33;
hence contradiction by A2, A3, ARYTM_1:10; :: thesis: verum

end;

then A5: not 0' - xx in {[0 ,0 ]} by TARSKI:def 1;
A6: xx -' 0' = (xx -' 0') + 0' by ARYTM_2:def 8
.= xx by A3, ARYTM_1:def 1 ;
0 in {0 } by TARSKI:def 1;
then A7: 0' - xx in [:{0 },REAL+ :] by A4, ZFMISC_1:106;
then 0' - xx in REAL+ \/ [:{0 },REAL+ :] by XBOOLE_0:def 3;
then reconsider b = 0' - xx as Element of REAL by A5, NUMBERS:def 1, XBOOLE_0:def 5;
consider x1, x2, y1, y2 being Element of REAL such that
A8: a = [*x1,x2*] and
A9: b = [*y1,y2*] and
A10: a + b = [*(+ x1,y1),(+ x2,y2)*] by XCMPLX_0:def 4;
+ x2,y2 = 0 by A10, ARYTM_0:26;
then A11: a + b = + x1,y1 by A10, ARYTM_0:def 7;
a in REAL by XREAL_0:def 1;
then x2 = 0 by A8, ARYTM_0:26;
then A12: a = x1 by A8, ARYTM_0:def 7;
y2 = 0 by A9, ARYTM_0:26;
then A13: b = y1 by A9, ARYTM_0:def 7;
then consider x', y' being Element of REAL+ such that
A14: x1 = x' and
A15: y1 = [0 ,y'] and
A16: + x1,y1 = x' - y' by A1, A7, A12, ARYTM_0:def 2;
y' = xx -' 0' by A4, A13, A15, ZFMISC_1:33;
then a + b = 0 by A1, A12, A11, A14, A16, A6, ARYTM_1:18;
hence 0' - xx = - a ; :: thesis: verum

end;

end;