let x, y be Surreal; :: thesis: ( not x == 0_No & x * y == 1_No implies y == x " )
assume A1: ( not x == 0_No & x * y == 1_No ) ; :: thesis: y == x "
then A2: x * (x ") == 1_No by Th33;
( ((x ") * x) * y == (x ") * (x * y) & (x ") * (x * y) == 1_No * (x ") ) by A1, SURREALR:54, SURREALR:69;
then ( 1_No * y == ((x ") * x) * y & ((x ") * x) * y == x " ) by A2, SURREALR:54, SURREALO:4;
hence y == x " by SURREALO:4; :: thesis: verum