let x be Surreal; :: thesis: for r being Real st r <> 0 holds
(x * (uReal . r)) * (uReal . (1 / r)) == x
let r be Real; :: thesis: ( r <> 0 implies (x * (uReal . r)) * (uReal . (1 / r)) == x )
assume r <> 0 ; :: thesis: (x * (uReal . r)) * (uReal . (1 / r)) == x
then (1 / r) * r = 1 by XCMPLX_1:106;
then (x * (uReal . r)) * (uReal . (1 / r)) == x * (uReal . 1) by Lm1;
hence (x * (uReal . r)) * (uReal . (1 / r)) == x by SURREALN:48; :: thesis: verum