let r be Real; :: thesis: uReal . r infinitely< No_omega
let s be positive Real; :: according to SURREALC:def 3 :: thesis: (uReal . r) * (uReal . s) < No_omega
A1: (r * s) + 0 < (r * s) + 1 by XREAL_1:6;
(uReal . r) * (uReal . s) == uReal . (r * s) by SURREALN:57;
then A2: (uReal . r) * (uReal . s) < uReal . ((r * s) + 1) by A1, SURREALN:51, SURREALO:4;
uReal . ((r * s) + 1) <= No_omega by Th1, SURREALN:76;
hence (uReal . r) * (uReal . s) < No_omega by A2, SURREALO:4; :: thesis: verum