let n be Element of NAT ; :: thesis:
A1: dom (dyad n) = Seg ((2 |^ n) + 1) by Def6;
for x being set holds
( x in rng (dyad n) iff x in dyadic n )

let x be set ; :: thesis:
A2: ( x in rng (dyad n) implies x in dyadic n )

assume x in rng (dyad n) ; :: thesis:
then consider y being set such that
A3: y in dom (dyad n) and
A4: x = (dyad n) . y by FUNCT_1:def 5;
A5: y in Seg ((2 |^ n) + 1) by A3, Def6;
reconsider y = y as Element of NAT by A3;
A6: 1 <= y by A5, FINSEQ_1:3;
then A7: 1 - 1 <= y - 1 by XREAL_1:15;
y <= (2 |^ n) + 1 by A5, FINSEQ_1:3;
then A8: y - 1 <= ((2 |^ n) + 1) - 1 by XREAL_1:15;
consider i being Nat such that
A9: 1 + i = y by A6, NAT_1:10;
( i in NAT & x = (y - 1) / (2 |^ n) ) by A3, A4, Def6, ORDINAL1:def 13;
hence x in dyadic n by A7, A8, A9, Def3; :: thesis:

end;

( x in dyadic n implies x in rng (dyad n) )

assume A10: x in dyadic n ; :: thesis:
then reconsider x = x as Real ;
consider i being Element of NAT such that
A11: ( 0 <= i & i <= 2 |^ n ) and
A12: x = i / (2 |^ n) by A10, Def3;
consider y being Element of NAT such that
A13: y = i + 1 ;
( 0 + 1 <= i + 1 & i + 1 <= (2 |^ n) + 1 ) by A11, XREAL_1:8;
then A14: y in Seg ((2 |^ n) + 1) by A13, FINSEQ_1:3;
then A15: y in dom (dyad n) by Def6;
x = (y - 1) / (2 |^ n) by A12, A13;
then x = (dyad n) . y by A1, A14, Def6;
hence x in rng (dyad n) by A15, FUNCT_1:def 5; :: thesis:

end;

hence ( x in rng (dyad n) iff x in dyadic n ) by A2; :: thesis:

end;