consider r being Real such that
A2: x == uReal . r by Th62;
consider s being Real such that
A3: y == uReal . s by Th62;
( x + y == (uReal . r) + (uReal . s) & (uReal . r) + (uReal . s) == uReal . (r + s) ) by A2, A3, SURREALR:66, Th55;
then x + y == uReal . (r + s) by SURREALO:4;
hence x + y is *real by Th62; :: thesis: verum