let a be Real; :: thesis: for Z9 being Element of REAL+ st Z9 = 0 holds

for x9 being Element of REAL+ st x9 = a holds

Z9 - x9 = - a

let Z9 be Element of REAL+ ; :: thesis: ( Z9 = 0 implies for x9 being Element of REAL+ st x9 = a holds

Z9 - x9 = - a )

assume A0: Z9 = 0 ; :: thesis: for x9 being Element of REAL+ st x9 = a holds

Z9 - x9 = - a

let xx be Element of REAL+ ; :: thesis: ( xx = a implies Z9 - xx = - a )

assume A1: xx = a ; :: thesis: Z9 - xx = - a

for x9 being Element of REAL+ st x9 = a holds

Z9 - x9 = - a

let Z9 be Element of REAL+ ; :: thesis: ( Z9 = 0 implies for x9 being Element of REAL+ st x9 = a holds

Z9 - x9 = - a )

assume A0: Z9 = 0 ; :: thesis: for x9 being Element of REAL+ st x9 = a holds

Z9 - x9 = - a

let xx be Element of REAL+ ; :: thesis: ( xx = a implies Z9 - xx = - a )

assume A1: xx = a ; :: thesis: Z9 - xx = - a

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

end;

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

set b = Z9 - xx;

A3: Z9 <=' xx by A0, ARYTM_1:6;

then not xx <=' Z9 by A0, A2, ARYTM_1:4;

then A4: Z9 - xx = [{},(xx -' Z9)] by ARYTM_1:def 2;

A6: xx -' Z9 = (xx -' Z9) + Z9 by A0, ARYTM_2:def 8

.= xx by A3, ARYTM_1:def 1 ;

0 in {0} by TARSKI:def 1;

then A7: Z9 - xx in [:{0},REAL+:] by A4, ZFMISC_1:87;

then Z9 - xx in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def 3;

then reconsider b = Z9 - 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;

a + b in REAL by XREAL_0:def 1;

then + (x2,y2) = 0 by A10, ARYTM_0:24;

then A11: a + b = + (x1,y1) by A10, ARYTM_0:def 5;

a in REAL by XREAL_0:def 1;

then x2 = 0 by A8, ARYTM_0:24;

then A12: a = x1 by A8, ARYTM_0:def 5;

y2 = 0 by A9, ARYTM_0:24;

then A13: b = y1 by A9, ARYTM_0:def 5;

then consider x9, y9 being Element of REAL+ such that

A14: x1 = x9 and

A15: y1 = [0,y9] and

A16: + (x1,y1) = x9 - y9 by A1, A7, A12, ARYTM_0:def 1;

y9 = xx -' Z9 by A4, A13, A15, XTUPLE_0:1;

then a + b = 0 by A1, A12, A11, A14, A16, A6, ARYTM_1:18;

hence Z9 - xx = - a ; :: thesis: verum

end;A3: Z9 <=' xx by A0, ARYTM_1:6;

then not xx <=' Z9 by A0, A2, ARYTM_1:4;

then A4: Z9 - xx = [{},(xx -' Z9)] by ARYTM_1:def 2;

now :: thesis: not Z9 - xx = [0,0]

then A5:
not Z9 - xx in {[0,0]}
by TARSKI:def 1;assume
Z9 - xx = [0,0]
; :: thesis: contradiction

then xx -' Z9 = 0 by A4, XTUPLE_0:1;

hence contradiction by A0, A2, A3, ARYTM_1:10; :: thesis: verum

end;then xx -' Z9 = 0 by A4, XTUPLE_0:1;

hence contradiction by A0, A2, A3, ARYTM_1:10; :: thesis: verum

A6: xx -' Z9 = (xx -' Z9) + Z9 by A0, ARYTM_2:def 8

.= xx by A3, ARYTM_1:def 1 ;

0 in {0} by TARSKI:def 1;

then A7: Z9 - xx in [:{0},REAL+:] by A4, ZFMISC_1:87;

then Z9 - xx in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def 3;

then reconsider b = Z9 - 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;

a + b in REAL by XREAL_0:def 1;

then + (x2,y2) = 0 by A10, ARYTM_0:24;

then A11: a + b = + (x1,y1) by A10, ARYTM_0:def 5;

a in REAL by XREAL_0:def 1;

then x2 = 0 by A8, ARYTM_0:24;

then A12: a = x1 by A8, ARYTM_0:def 5;

y2 = 0 by A9, ARYTM_0:24;

then A13: b = y1 by A9, ARYTM_0:def 5;

then consider x9, y9 being Element of REAL+ such that

A14: x1 = x9 and

A15: y1 = [0,y9] and

A16: + (x1,y1) = x9 - y9 by A1, A7, A12, ARYTM_0:def 1;

y9 = xx -' Z9 by A4, A13, A15, XTUPLE_0:1;

then a + b = 0 by A1, A12, A11, A14, A16, A6, ARYTM_1:18;

hence Z9 - xx = - a ; :: thesis: verum