let y be Surreal; :: thesis: for r being Real st r <> 0 holds
not (uReal . r) * (No_omega^ y) == 0_No
let r be Real; :: thesis: ( r <> 0 implies not (uReal . r) * (No_omega^ y) == 0_No )
assume r <> 0 ; :: thesis: not (uReal . r) * (No_omega^ y) == 0_No
then |.((uReal . r) * (No_omega^ y)).|, No_omega^ y are_commensurate by Th66;
then |.((uReal . r) * (No_omega^ y)).| is positive by Th3;
hence not (uReal . r) * (No_omega^ y) == 0_No by Def6; :: thesis: verum