:: deftheorem Def6 defines divR SURREALI:def 6 :
for x being object
for Inv, b₃ being Function holds
( b₃ = divR (x,Inv) iff ( dom b₃ = NAT & ( for k being Nat holds b₃ . k = ((transitions_of (x,Inv)) . k) `2 ) ) );