let x be Surreal; :: thesis: ( not x == 0_No implies omega-y x = omega-y (- x) )
assume A1: not x == 0_No ; :: thesis: omega-y x = omega-y (- x)
then A2: |.x.|, No_omega^ (omega-y x) are_commensurate by Def7;
A3: |.x.| = |.(- x).| by A1, Th39;
not - x == 0_No by A1, SURREALR:24;
hence omega-y x = omega-y (- x) by A2, A3, Def7; :: thesis: verum