reconsider y9 = 0 as Element of REAL+ by ARYTM_2:20;
let x, o be Element of REAL ; :: thesis: ( o = 0 implies + (x,o) = x )
assume A1: o = 0 ; :: thesis: + (x,o) = x

per cases ( x in REAL+ or not x in REAL+ ) ;

suppose x in REAL+ ; :: thesis: + (x,o) = x

then reconsider x9 = x as Element of REAL+ ;
x9 = x9 + y9 by ARYTM_2:def 8;
hence + (x,o) = x by A1, Def1; :: thesis: verum

end;

suppose A2: not x in REAL+ ; :: thesis: + (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; :: thesis: verum

end;

end;