let T be full Tree; :: thesis: for n being non zero Nat holds Seg (2 to_power n) c= rng (NumberOnLevel (n,T))
let n be non zero Nat; :: thesis: Seg (2 to_power n) c= rng (NumberOnLevel (n,T))
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Seg (2 to_power n) or y in rng (NumberOnLevel (n,T)) )
assume y in Seg (2 to_power n) ; :: thesis: 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 ;
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 ;
then k - 1 < 2 to_power n by XREAL_1:19;
then A8: k -' 1 < 2 to_power n by ;
(NumberOnLevel (n,T)) . (Rev (n -BinarySequence (k -' 1))) = () + 1 by
.= (Absval (n -BinarySequence (k -' 1))) + 1
.= (k -' 1) + 1 by
.= (k - 1) + 1 by
.= y by A1 ;
hence y in rng (NumberOnLevel (n,T)) by ; :: thesis: verum