let T be full Tree; for n being non empty Nat holds Seg (2 to_power n) c= rng (NumberOnLevel n,T)
let n be non empty Nat; Seg (2 to_power n) c= rng (NumberOnLevel n,T)
let y be set ; 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 Element of NAT : ( 1 <= k & k <= 2 to_power n ) }
by FINSEQ_1:def 1;
then consider k being Element of 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:11;
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 FINSEQ_1:def 18
;
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:110;
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:21;
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
by FINSEQ_6:29
.=
(k -' 1) + 1
by A8, BINARI_3:36
.=
(k - 1) + 1
by A4, XREAL_0:def 2
.=
y
by A1
;
hence
y in rng (NumberOnLevel n,T)
by A7, FUNCT_1:def 5; verum