let x, y be Surreal; :: thesis: ( |.y.| infinitely< |.x.| implies ( not x == 0_No & not x + y == 0_No & omega-y x = omega-y (x + y) & omega-r x = omega-r (x + y) ) )
assume A1: |.y.| infinitely< |.x.| ; :: thesis: ( not x == 0_No & not x + y == 0_No & omega-y x = omega-y (x + y) & omega-r x = omega-r (x + y) )
hence A2: ( not x == 0_No & not x + y == 0_No ) by Th45, Th47; :: thesis: ( omega-y x = omega-y (x + y) & omega-r x = omega-r (x + y) )
A3: |.y.| * (uReal . ((2 + 1) / 2)) < |.x.| by A1;
then |.x.|,|.(x + y).| are_commensurate by Th57;
hence A4: omega-y x = omega-y (x + y) by A2, Th61; :: thesis: omega-r x = omega-r (x + y)
set N = No_omega^ (omega-y x);
A5: |.(x - ((No_omega^ (omega-y x)) * (uReal . (omega-r x)))).| infinitely< |.x.| by A2, Def8;
|.((x + y) + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x))))).| infinitely< |.x.|

proof

let s be positive Real; :: according to SURREALC:def 3 :: thesis: |.((x + y) + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x))))).| * (uReal . s) < |.x.|
A6: 0_No <= uReal . s by SURREALI:def 8;
set r = uReal . (omega-r x);
(x + y) + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x)))) = y + (x + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x))))) by SURREALR:37;
then ( |.((x + y) + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x))))).| * (uReal . s) <= (|.(x + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x))))).| + |.y.|) * (uReal . s) & (|.(x + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x))))).| + |.y.|) * (uReal . s) == (|.(x + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x))))).| * (uReal . s)) + (|.y.| * (uReal . s)) ) by Th37, A6, SURREALR:67, SURREALR:75;
then A7: |.((x + y) + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x))))).| * (uReal . s) <= (|.(x + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x))))).| * (uReal . s)) + (|.y.| * (uReal . s)) by SURREALO:4;
A8: |.x.| = |.x.| * (uReal . 1) by SURREALN:48;
|.(x + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x))))).| * (uReal . (s * 2)) < |.x.| by A5;
then A9: |.(x + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x))))).| * (uReal . ((s * 2) * (1 / 2))) <= |.x.| * (uReal . (1 * (1 / 2))) by Th59, A8;
|.y.| * (uReal . (s * 2)) < |.x.| by A1;
then |.y.| * (uReal . ((s * 2) * (1 / 2))) < |.x.| * (uReal . (1 * (1 / 2))) by Th59, A8;
then A10: (|.(x + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x))))).| * (uReal . s)) + (|.y.| * (uReal . s)) < (|.x.| * (uReal . (1 * (1 / 2)))) + (|.x.| * (uReal . (1 * (1 / 2)))) by A9, SURREALR:44;
( (|.x.| * (uReal . (1 * (1 / 2)))) + (|.x.| * (uReal . (1 * (1 / 2)))) == |.x.| * ((uReal . (1 / 2)) + (uReal . (1 / 2))) & |.x.| * ((uReal . (1 / 2)) + (uReal . (1 / 2))) == |.x.| * (uReal . ((1 / 2) + (1 / 2))) ) by SURREALR:67, SURREALR:51, SURREALN:55;
then ( (|.x.| * (uReal . (1 * (1 / 2)))) + (|.x.| * (uReal . (1 * (1 / 2)))) == |.x.| * (uReal . 1) & |.x.| * (uReal . 1) = |.x.| ) by SURREALN:48, SURREALO:4;
then (|.(x + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x))))).| * (uReal . s)) + (|.y.| * (uReal . s)) < |.x.| by A10, SURREALO:4;
hence |.((x + y) + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x))))).| * (uReal . s) < |.x.| by A7, SURREALO:4; :: thesis: verum

end;

then |.((x + y) - ((No_omega^ (omega-y x)) * (uReal . (omega-r x)))).| infinitely< |.(x + y).| by A3, Th57, Th16;
hence omega-r x = omega-r (x + y) by A2, A4, Def8; :: thesis: verum