let T be full Tree; for n being non zero Nat holds Seg (2 to_power n) c= rng (NumberOnLevel (n,T))
let n be non zero Nat; Seg (2 to_power n) c= rng (NumberOnLevel (n,T))
let y be object ; TARSKI:def 3 ( not y in Seg (2 to_power n) or y in rng (NumberOnLevel (n,T)) )
assume
y in Seg (2 to_power n)
; y in rng (NumberOnLevel (n,T))
then
y in { k where k is Nat : ( 1 <= k & k <= 2 to_power n ) }
by FINSEQ_1:def 1;
then consider k being Nat such that
A1:
k = y
and
A2:
1 <= k
and
A3:
k <= 2 to_power n
;
A4:
k - 1 >= 1 - 1
by A2, XREAL_1:9;
set t = Rev (n -BinarySequence (k -' 1));
A5: len (Rev (n -BinarySequence (k -' 1))) =
len (n -BinarySequence (k -' 1))
by FINSEQ_5:def 3
.=
n
by CARD_1:def 7
;
then
len (Rev (Rev (n -BinarySequence (k -' 1)))) = n
by FINSEQ_5:def 3;
then reconsider F = Rev (Rev (n -BinarySequence (k -' 1))) as Element of n -tuples_on BOOLEAN by FINSEQ_2:92;
T = {0,1} *
by Def2;
then
Rev (n -BinarySequence (k -' 1)) in T
by FINSEQ_1:def 11;
then
Rev (n -BinarySequence (k -' 1)) in { w where w is Element of T : len w = n }
by A5;
then A6:
Rev (n -BinarySequence (k -' 1)) in T -level n
by TREES_2:def 6;
then A7:
Rev (n -BinarySequence (k -' 1)) in dom (NumberOnLevel (n,T))
by FUNCT_2:def 1;
k < (2 to_power n) + 1
by A3, NAT_1:13;
then
k - 1 < 2 to_power n
by XREAL_1:19;
then A8:
k -' 1 < 2 to_power n
by A4, XREAL_0:def 2;
(NumberOnLevel (n,T)) . (Rev (n -BinarySequence (k -' 1))) =
(Absval F) + 1
by A6, Def1
.=
(Absval (n -BinarySequence (k -' 1))) + 1
.=
(k -' 1) + 1
by A8, BINARI_3:35
.=
(k - 1) + 1
by A4, XREAL_0:def 2
.=
y
by A1
;
hence
y in rng (NumberOnLevel (n,T))
by A7, FUNCT_1:def 3; verum