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

proof

let x be set ; :: 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 set such that
A3: ( y in dom (dyad n) & x = (dyad n) . y ) by FUNCT_1:def 5;
A4: y in Seg ((2 |^ n) + 1) by A3, Def6;
reconsider y = y as Element of NAT by A3;
A5: ( 1 <= y & y <= (2 |^ n) + 1 ) by A4, FINSEQ_1:3;
then A6: ( 1 - 1 <= y - 1 & y - 1 <= ((2 |^ n) + 1) - 1 ) by XREAL_1:15;
consider i being Nat such that
A7: 1 + i = y by A5, NAT_1:10;
A8: i in NAT by ORDINAL1:def 13;
x = (y - 1) / (2 |^ n) by A3, Def6;
hence x in dyadic n by A6, A7, A8, Def3; :: 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 Element of NAT such that
A10: ( 0 <= i & i <= 2 |^ n & x = i / (2 |^ n) ) by A9, Def3;
A11: ( 0 + 1 <= i + 1 & i + 1 <= (2 |^ n) + 1 ) by A10, XREAL_1:8;
consider y being Element of NAT such that
A12: y = i + 1 ;
A13: y in Seg ((2 |^ n) + 1) by A11, A12, FINSEQ_1:3;
then A14: y in dom (dyad n) by Def6;
x = (y - 1) / (2 |^ n) by A10, A12;
then x = (dyad n) . y by A1, A13;
hence x in rng (dyad n) by A14, FUNCT_1:def 5; :: 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 Def6, TARSKI:2; :: thesis: verum