consider r being Real such that
A4: x == uReal . r by Th62;
consider s being Real such that
A5: y == uReal . s by Th62;
( x * y == (uReal . r) * y & (uReal . r) * y == (uReal . r) * (uReal . s) ) by A4, A5, SURREALR:54;
then ( x * y == (uReal . r) * (uReal . s) & (uReal . r) * (uReal . s) == uReal . (r * s) ) by SURREALO:4, Th57;
then x * y == uReal . (r * s) by SURREALO:4;
hence x * y is *real by Th62; :: thesis: verum