let x, y be Surreal; :: thesis: for r1, r2 being Real st |.x.|, No_omega^ y are_commensurate & |.(x - ((No_omega^ y) * (uReal . r1))).| infinitely< |.x.| & |.(x - ((No_omega^ y) * (uReal . r2))).| infinitely< |.x.| holds
r2 = r1
let r1, r2 be Real; :: thesis: ( |.x.|, No_omega^ y are_commensurate & |.(x - ((No_omega^ y) * (uReal . r1))).| infinitely< |.x.| & |.(x - ((No_omega^ y) * (uReal . r2))).| infinitely< |.x.| implies r2 = r1 )
set X = |.x.|;
set N = No_omega^ y;
assume A1: ( |.x.|, No_omega^ y are_commensurate & |.(x - ((No_omega^ y) * (uReal . r1))).| infinitely< |.x.| & |.(x - ((No_omega^ y) * (uReal . r2))).| infinitely< |.x.| ) ; :: thesis: r2 = r1
reconsider X = |.x.| as positive Surreal by A1, Th3;

per cases ( X = x or X = - x ) by Def6;

suppose X = x ; :: thesis: r2 = r1

then ( r1 <= r2 & r2 <= r1 ) by A1, Lm8;
hence r2 = r1 by XXREAL_0:1; :: thesis: verum

end;

suppose A2: X = - x ; :: thesis: r2 = r1

then A3: x + (- ((No_omega^ y) * (uReal . r1))) = (- X) + (- ((No_omega^ y) * (uReal . r1)))
.= - (X + ((No_omega^ y) * (uReal . r1))) by SURREALR:40 ;
- (uReal . (- r1)) == uReal . (- (- r1)) by SURREALN:56;
then ( - ((No_omega^ y) * (uReal . (- r1))) = (No_omega^ y) * (- (uReal . (- r1))) & (No_omega^ y) * (- (uReal . (- r1))) == (No_omega^ y) * (uReal . r1) ) by SURREALR:51, SURREALR:58;
then X + ((No_omega^ y) * (uReal . r1)) == X + (- ((No_omega^ y) * (uReal . (- r1)))) by SURREALR:43;
then x + (- ((No_omega^ y) * (uReal . r1))) == - (X + (- ((No_omega^ y) * (uReal . (- r1))))) by A3, SURREALR:10;
then ( |.(x + (- ((No_omega^ y) * (uReal . r1)))).| == |.(- (X + (- ((No_omega^ y) * (uReal . (- r1)))))).| & |.(- (X + (- ((No_omega^ y) * (uReal . (- r1)))))).| == |.(X + (- ((No_omega^ y) * (uReal . (- r1))))).| ) by Th48, Th39, Th38;
then |.(x + (- ((No_omega^ y) * (uReal . r1)))).| == |.(X + (- ((No_omega^ y) * (uReal . (- r1))))).| by SURREALO:4;
then A4: |.(X - ((No_omega^ y) * (uReal . (- r1)))).| infinitely< X by A1, Th17;
A5: x + (- ((No_omega^ y) * (uReal . r2))) = (- X) + (- ((No_omega^ y) * (uReal . r2))) by A2
.= - (X + ((No_omega^ y) * (uReal . r2))) by SURREALR:40 ;
- (uReal . (- r2)) == uReal . (- (- r2)) by SURREALN:56;
then ( - ((No_omega^ y) * (uReal . (- r2))) = (No_omega^ y) * (- (uReal . (- r2))) & (No_omega^ y) * (- (uReal . (- r2))) == (No_omega^ y) * (uReal . r2) ) by SURREALR:51, SURREALR:58;
then X + ((No_omega^ y) * (uReal . r2)) == X + (- ((No_omega^ y) * (uReal . (- r2)))) by SURREALR:43;
then x + (- ((No_omega^ y) * (uReal . r2))) == - (X + (- ((No_omega^ y) * (uReal . (- r2))))) by A5, SURREALR:10;
then ( |.(x + (- ((No_omega^ y) * (uReal . r2)))).| == |.(- (X + (- ((No_omega^ y) * (uReal . (- r2)))))).| & |.(- (X + (- ((No_omega^ y) * (uReal . (- r2)))))).| == |.(X + (- ((No_omega^ y) * (uReal . (- r2))))).| ) by Th48, Th39, Th38;
then |.(x + (- ((No_omega^ y) * (uReal . r2)))).| == |.(X + (- ((No_omega^ y) * (uReal . (- r2))))).| by SURREALO:4;
then |.(X - ((No_omega^ y) * (uReal . (- r2)))).| infinitely< X by A1, Th17;
then ( - r1 <= - r2 & - r2 <= - r1 ) by A4, A1, Lm8;
then - r1 = - r2 by XXREAL_0:1;
hence r2 = r1 ; :: thesis: verum

end;

end;