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

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

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

then reconsider x' = x as Element of REAL+ ;
x' = x' + y' by ARYTM_2:def 8;
hence + x,o = x by A1, Def2; :: thesis: verum

end;

suppose A2: not x in REAL+ ; :: thesis: + x,o = x

x in REAL+ \/ [:{{} },REAL+ :] by NUMBERS:def 1, XBOOLE_0:def 5;
then A3: x in [:{{} },REAL+ :] by A2, XBOOLE_0:def 3;
then consider x1, x2 being set such that
A4: x1 in {{} } and
A5: x2 in REAL+ and
A6: x = [x1,x2] by ZFMISC_1:103;
reconsider x' = x2 as Element of REAL+ by A5;
A7: x1 = 0 by A4, TARSKI:def 1;
then x = y' - x' by A6, Th3, ARYTM_1:19;
hence + x,o = x by A1, A3, A6, A7, Def2; :: thesis: verum

end;

end;