:: deftheorem Def13 defines No_inverses_on SURREALI:def 13 :
for x being Surreal
for b₂ being Function holds
( b₂ = No_inverses_on x iff ( dom b₂ = ((L_ x) \/ (R_ x)) \ {0_No} & ( for y being Surreal st y in ((L_ x) \/ (R_ x)) \ {0_No} holds
b₂ . y = inv y ) ) );