theorem Th9: :: SURREALS:9

for n being Nat
for o being object
for p being pair object st L_ p is surreal-membered & R_ p is surreal-membered holds
( (sqrtL (p,o)) . n is surreal-membered & (sqrtR (p,o)) . n is surreal-membered )