let x, y be Surreal; :: thesis: ( x == y & not x == 0_No implies ( omega-y x = omega-y y & omega-r x = omega-r y ) )
assume A1: ( x == y & not x == 0_No ) ; :: thesis: ( omega-y x = omega-y y & omega-r x = omega-r y )
A2: not y == 0_No by A1, SURREALO:4;
|.x.| is positive by A1, Th36;
then A3: |.x.|,|.y.| are_commensurate by A1, Th48, Th8;
then A4: omega-y x = omega-y y by A2, A1, Th61;
set rx = omega-r x;
|.(x - ((No_omega^ (omega-y x)) * (uReal . (omega-r x)))).| infinitely< |.x.| by A1, Def8;
then A5: |.(x + (- ((No_omega^ (omega-y y)) * (uReal . (omega-r x))))).| infinitely< |.y.| by A4, A3, Th16;
x + (- ((No_omega^ (omega-y y)) * (uReal . (omega-r x)))) == y + (- ((No_omega^ (omega-y y)) * (uReal . (omega-r x)))) by SURREALR:43, A1;
then |.(y - ((No_omega^ (omega-y y)) * (uReal . (omega-r x)))).| infinitely< |.y.| by A5, Th17, Th48;
hence ( omega-y x = omega-y y & omega-r x = omega-r y ) by A2, Def8, A3, A1, Th61; :: thesis: verum