:: deftheorem Def5 defines sqrtR SURREALS:def 5 :
for x0 being pair object
for x being object
for b₃ being Function holds
( b₃ = sqrtR (x0,x) iff ( dom b₃ = NAT & ( for k being Nat holds b₃ . k = ((transitions_of (x0,x)) . k) `2 ) ) );