reconsider y9 = 0 as Element of REAL+ by ARYTM_2:20;
let x, o be Element of REAL ; ( o = 0 implies + (x,o) = x )
assume A1:
o = 0
; + (x,o) = x
per cases
( x in REAL+ or not x in REAL+ )
;
suppose A2:
not
x in REAL+
;
+ (x,o) = x
x in REAL+ \/ [:{{}},REAL+:]
by XBOOLE_0:def 5;
then A3:
x in [:{{}},REAL+:]
by A2, XBOOLE_0:def 3;
then consider x1,
x2 being
object such that A4:
x1 in {{}}
and A5:
x2 in REAL+
and A6:
x = [x1,x2]
by ZFMISC_1:84;
reconsider x9 =
x2 as
Element of
REAL+ by A5;
A7:
x1 = 0
by A4, TARSKI:def 1;
then
x = y9 - x9
by A6, Th3, ARYTM_1:19;
hence
+ (
x,
o)
= x
by A1, A3, A6, A7, Def1;
verum end; end;