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 )

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

hence
( dom (dyad n) = Seg ((2 |^ n) + 1) & rng (dyad n) = dyadic n )
by Def4, TARSKI:2; :: thesis: verum
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 )

end;A2: ( x in rng (dyad n) implies x in dyadic n )

proof

( x in dyadic n implies x in rng (dyad n) )
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;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

proof

hence
( x in rng (dyad n) iff x in dyadic n )
by A2; :: thesis: verum
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;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