theorem Th9: :: SURREALI:9

for n being Nat
for x being Surreal
for Inv being Function st Inv is ((L_ x) \/ (R_ x)) \ {0_No} -surreal-valued holds
( (divL (x,Inv)) . n is surreal-membered & (divR (x,Inv)) . n is surreal-membered )