let n be Nat; :: thesis: ( dom (dyad n) = Seg ((2 |^ n) + 1) & rng (dyad n) = dyadic n )
A1: dom (dyad n) = Seg ((2 |^ n) + 1) by Def4;
for x being object holds
( x in rng (dyad n) iff x in dyadic n )

proof

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

proof

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

end;

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

proof

assume A9: x in dyadic n ; :: thesis: x in rng (dyad n)
then reconsider x = x as Real ;
consider i being Nat such that
A10: i <= 2 |^ n and
A11: x = i / (2 |^ n) by A9, Def1;
consider y being Nat such that
A12: y = i + 1 ;
( 0 + 1 <= i + 1 & i + 1 <= (2 |^ n) + 1 ) by A10, XREAL_1:6;
then A13: y in Seg ((2 |^ n) + 1) by A12, FINSEQ_1:1;
then A14: y in dom (dyad n) by Def4;
x = (y - 1) / (2 |^ n) by A11, A12;
then x = (dyad n) . y by A1, A13, Def4;
hence x in rng (dyad n) by A14, FUNCT_1:def 3; :: thesis: verum

end;

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

end;

hence ( dom (dyad n) = Seg ((2 |^ n) + 1) & rng (dyad n) = dyadic n ) by Def4, TARSKI:2; :: thesis: verum