let x, y be Surreal; :: thesis: for r being Real st 0_No <= x & x infinitely< y holds
|.((uReal . r) * x).| infinitely< y
let r be Real; :: thesis: ( 0_No <= x & x infinitely< y implies |.((uReal . r) * x).| infinitely< y )
assume A1: ( 0_No <= x & x infinitely< y ) ; :: thesis: |.((uReal . r) * x).| infinitely< y

per cases ( r > 0 or r < 0 or r = 0 ) ;

suppose A2: r > 0 ; :: thesis: |.((uReal . r) * x).| infinitely< y

then uReal . r >= 0_No by SURREALN:47, SURREALN:51;
then (uReal . r) * x >= 0_No * x by A1, SURREALR:75;
then |.((uReal . r) * x).| = (uReal . r) * x by SURREALC:def 6;
hence |.((uReal . r) * x).| infinitely< y by A1, A2, SURREALC:13; :: thesis: verum

end;

suppose A3: r < 0 ; :: thesis: |.((uReal . r) * x).| infinitely< y

then uReal . (- r) >= 0_No by SURREALN:47, SURREALN:51;
then (uReal . (- r)) * x >= 0_No * x by A1, SURREALR:75;
then |.((uReal . (- r)) * x).| = (uReal . (- r)) * x by SURREALC:def 6;
then A4: |.((uReal . (- r)) * x).| infinitely< y by A1, A3, SURREALC:13;
(uReal . (- r)) * x == (- (uReal . r)) * x by SURREALR:54, SURREALN:56;
then (uReal . (- r)) * x == - ((uReal . r) * x) by SURREALR:58;
then ( |.((uReal . (- r)) * x).| == |.(- ((uReal . r) * x)).| & |.(- ((uReal . r) * x)).| == |.((uReal . r) * x).| ) by SURREALC:40, SURREALC:48;
then |.((uReal . (- r)) * x).| == |.((uReal . r) * x).| by SURREALO:9;
hence |.((uReal . r) * x).| infinitely< y by A4, SURREALC:17; :: thesis: verum

end;

suppose A5: r = 0 ; :: thesis: |.((uReal . r) * x).| infinitely< y

0_No infinitely< y

proof

let e be positive Real; :: according to SURREALC:def 3 :: thesis: not y <= 0_No * (uReal . e)
thus not y <= 0_No * (uReal . e) by A1, SURREALC:9, SURREALO:9; :: thesis: verum

end;

hence |.((uReal . r) * x).| infinitely< y by A5, SURREALN:47, SURREALC:def 6; :: thesis: verum

end;

end;