:: deftheorem Def5 defines divL SURREALI:def 5 :
for x being object
for Inv, b₃ being Function holds
( b₃ = divL (x,Inv) iff ( dom b₃ = NAT & ( for k being Nat holds b₃ . k = ((transitions_of (x,Inv)) . k) `1 ) ) );