theorem Th8: :: SURREALS:8

for n being Nat
for o being object
for p being pair object holds
( (sqrtL (p,o)) . (n + 1) = ((sqrtL (p,o)) . n) \/ (sqrt (o,((sqrtL (p,o)) . n),((sqrtR (p,o)) . n))) & (sqrtR (p,o)) . (n + 1) = (((sqrtR (p,o)) . n) \/ (sqrt (o,((sqrtL (p,o)) . n),((sqrtL (p,o)) . n)))) \/ (sqrt (o,((sqrtR (p,o)) . n),((sqrtR (p,o)) . n))) )