:: deftheorem Def4 defines dyad URYSOHN1:def 4 :
for n being Nat
for b₂ being FinSequence holds
( b₂ = dyad n iff ( dom b₂ = Seg ((2 |^ n) + 1) & ( for i being Nat st i in dom b₂ holds
b₂ . i = (i - 1) / (2 |^ n) ) ) );