let x be Surreal; :: thesis: for r being Real st x is positive & r <> 0 holds
|.((uReal . r) * x).|,x are_commensurate
let r be Real; :: thesis: ( x is positive & r <> 0 implies |.((uReal . r) * x).|,x are_commensurate )
assume A1: ( x is positive & r <> 0 ) ; :: thesis: |.((uReal . r) * x).|,x are_commensurate

per cases then ( 0 < r or r < 0 ) ;

suppose A2: 0 < r ; :: thesis: |.((uReal . r) * x).|,x are_commensurate

then 0_No <= (uReal . r) * x by A1, SURREALI:def 8;
then (uReal . r) * x = |.((uReal . r) * x).| by Def6;
hence |.((uReal . r) * x).|,x are_commensurate by Lm10, A1, A2; :: thesis: verum

end;

suppose A3: r < 0 ; :: thesis: |.((uReal . r) * x).|,x are_commensurate

0_No <= (uReal . (- r)) * x by A3, A1, SURREALI:def 8;
then A4: (uReal . (- r)) * x = |.((uReal . (- r)) * x).| by Def6;
( (uReal . (- r)) * x == (- (uReal . r)) * x & (- (uReal . r)) * x == - ((uReal . r) * x) ) by SURREALN:56, SURREALR:51, SURREALR:58;
then (uReal . (- r)) * x == - ((uReal . r) * x) by SURREALR:58;
then ( |.((uReal . (- r)) * x).| == |.(- ((uReal . r) * x)).| & |.(- ((uReal . r) * x)).| == |.((uReal . r) * x).| ) by Th48, Th39, Th38;
then (uReal . (- r)) * x == |.((uReal . r) * x).| by A4, SURREALO:4;
hence |.((uReal . r) * x).|,x are_commensurate by A3, Lm10, A1, Th5; :: thesis: verum

end;

end;