let y be Surreal; :: thesis: for r being Real st r <> 0 holds
omega-y ((uReal . r) * (No_omega^ y)) = Unique_No y
let r be Real; :: thesis: ( r <> 0 implies omega-y ((uReal . r) * (No_omega^ y)) = Unique_No y )
assume r <> 0 ; :: thesis: omega-y ((uReal . r) * (No_omega^ y)) = Unique_No y
then A1: ( |.((uReal . r) * (No_omega^ y)).|, No_omega^ y are_commensurate & not (uReal . r) * (No_omega^ y) == 0_No ) by Th66, Th67;
y == Unique_No y by SURREALO:def 10;
then No_omega^ y == No_omega^ (Unique_No y) by Lm5;
then |.((uReal . r) * (No_omega^ y)).|, No_omega^ (Unique_No y) are_commensurate by A1, Th5;
hence omega-y ((uReal . r) * (No_omega^ y)) = Unique_No y by A1, Def7; :: thesis: verum