:: deftheorem Def4 defines sqrtL SURREALS:def 4 :
for x0 being pair object
for x being object
for b₃ being Function holds
( b₃ = sqrtL (x0,x) iff ( dom b₃ = NAT & ( for k being Nat holds b₃ . k = ((transitions_of (x0,x)) . k) `1 ) ) );