theorem :: URYSOHN1:4

for n being Nat holds
( dom (dyad n) = Seg ((2 |^ n) + 1) & rng (dyad n) = dyadic n )