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