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 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; :: thesis: verum

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 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; :: thesis: verum