let x be R_eal; :: thesis: ( x + 0. = x & 0. + x = x )
A1: ( x in REAL or x = -infty or x = +infty ) by XXREAL_0:14;
( x in REAL implies ( x + 0. = x & 0. + x = x ) )

proof

assume x in REAL ; :: thesis: ( x + 0. = x & 0. + x = x )
then reconsider a = x as Real ;
x + 0. = a + 0 by Def2
.= x ;
hence ( x + 0. = x & 0. + x = x ) ; :: thesis: verum

end;

hence ( x + 0. = x & 0. + x = x ) by A1, Def2; :: thesis: verum