let x be Surreal; :: thesis: (No_omega^ x) " == No_omega^ (- x)
set X = No_omega^ x;
A1: not No_omega^ x == 0_No by SURREALI:def 8;
x - x == 0_No by SURREALR:39;
then A2: ( No_omega^ (x - x) == No_omega^ 0_No & No_omega^ 0_No = 1_No ) by Th26, Lm5;
(No_omega^ x) * (No_omega^ (- x)) == No_omega^ (x - x) by Th27;
then ( (No_omega^ x) * (No_omega^ (- x)) == No_omega^ 0_No & No_omega^ 0_No = 1_No ) by A2, SURREALO:4;
hence (No_omega^ x) " == No_omega^ (- x) by SURREALI:42, A1; :: thesis: verum