let T be full Tree; :: thesis: for n being non zero Nat

for i being Nat st i in Seg (2 to_power n) holds

(FinSeqLevel (n,T)) . i = Rev (n -BinarySequence (i -' 1))

let n be non zero Nat; :: thesis: for i being Nat st i in Seg (2 to_power n) holds

(FinSeqLevel (n,T)) . i = Rev (n -BinarySequence (i -' 1))

let i be Nat; :: thesis: ( i in Seg (2 to_power n) implies (FinSeqLevel (n,T)) . i = Rev (n -BinarySequence (i -' 1)) )

reconsider nB = n -BinarySequence (i -' 1) as Element of n -tuples_on BOOLEAN by FINSEQ_2:131;

assume A1: i in Seg (2 to_power n) ; :: thesis: (FinSeqLevel (n,T)) . i = Rev (n -BinarySequence (i -' 1))

then A2: 1 <= i by FINSEQ_1:1;

i <= 2 to_power n by A1, FINSEQ_1:1;

then i < (2 to_power n) + 1 by NAT_1:13;

then i - 1 < 2 to_power n by XREAL_1:19;

then i -' 1 < 2 to_power n by A2, XREAL_1:233;

then A3: (Absval nB) + 1 = (i -' 1) + 1 by BINARI_3:35

.= (i - 1) + 1 by A2, XREAL_1:233

.= i ;

A4: len (Rev nB) = len nB by FINSEQ_5:def 3

.= n by CARD_1:def 7 ;

then reconsider RnB = Rev nB as Element of n -tuples_on BOOLEAN by FINSEQ_2:92;

RnB in {0,1} * by FINSEQ_1:def 11;

then RnB is Element of T by Def2;

then RnB in { t where t is Element of T : len t = n } by A4;

then A5: RnB in T -level n by TREES_2:def 6;

nB = Rev RnB ;

then A6: (NumberOnLevel (n,T)) . RnB = (Absval nB) + 1 by A5, Def1;

RnB in dom (NumberOnLevel (n,T)) by A5, FUNCT_2:def 1;

hence (FinSeqLevel (n,T)) . i = Rev (n -BinarySequence (i -' 1)) by A6, A3, FUNCT_1:32; :: thesis: verum

for i being Nat st i in Seg (2 to_power n) holds

(FinSeqLevel (n,T)) . i = Rev (n -BinarySequence (i -' 1))

let n be non zero Nat; :: thesis: for i being Nat st i in Seg (2 to_power n) holds

(FinSeqLevel (n,T)) . i = Rev (n -BinarySequence (i -' 1))

let i be Nat; :: thesis: ( i in Seg (2 to_power n) implies (FinSeqLevel (n,T)) . i = Rev (n -BinarySequence (i -' 1)) )

reconsider nB = n -BinarySequence (i -' 1) as Element of n -tuples_on BOOLEAN by FINSEQ_2:131;

assume A1: i in Seg (2 to_power n) ; :: thesis: (FinSeqLevel (n,T)) . i = Rev (n -BinarySequence (i -' 1))

then A2: 1 <= i by FINSEQ_1:1;

i <= 2 to_power n by A1, FINSEQ_1:1;

then i < (2 to_power n) + 1 by NAT_1:13;

then i - 1 < 2 to_power n by XREAL_1:19;

then i -' 1 < 2 to_power n by A2, XREAL_1:233;

then A3: (Absval nB) + 1 = (i -' 1) + 1 by BINARI_3:35

.= (i - 1) + 1 by A2, XREAL_1:233

.= i ;

A4: len (Rev nB) = len nB by FINSEQ_5:def 3

.= n by CARD_1:def 7 ;

then reconsider RnB = Rev nB as Element of n -tuples_on BOOLEAN by FINSEQ_2:92;

RnB in {0,1} * by FINSEQ_1:def 11;

then RnB is Element of T by Def2;

then RnB in { t where t is Element of T : len t = n } by A4;

then A5: RnB in T -level n by TREES_2:def 6;

nB = Rev RnB ;

then A6: (NumberOnLevel (n,T)) . RnB = (Absval nB) + 1 by A5, Def1;

RnB in dom (NumberOnLevel (n,T)) by A5, FUNCT_2:def 1;

hence (FinSeqLevel (n,T)) . i = Rev (n -BinarySequence (i -' 1)) by A6, A3, FUNCT_1:32; :: thesis: verum