:: deftheorem defines No_omega^ SURREALC:def 5 :
for x being Surreal holds No_omega^ x = (No_omega_op (born x)) . x;