let T be full Tree; :: thesis: for n being non empty Element of NAT
for i being Element of NAT st i in Seg (2 to_power n) holds
(FinSeqLevel n,T) . i = Rev (n -BinarySequence (i -' 1))
let n be non empty Element of NAT ; :: thesis: for i being Element of NAT st i in Seg (2 to_power n) holds
(FinSeqLevel n,T) . i = Rev (n -BinarySequence (i -' 1))
let i be Element of NAT ; :: thesis: ( i in Seg (2 to_power n) implies (FinSeqLevel n,T) . i = Rev (n -BinarySequence (i -' 1)) )
assume i in Seg (2 to_power n) ; :: thesis: (FinSeqLevel n,T) . i = Rev (n -BinarySequence (i -' 1))
then A1: ( 1 <= i & i <= 2 to_power n ) by FINSEQ_1:3;
set nB = n -BinarySequence (i -' 1);
A2: len (Rev (n -BinarySequence (i -' 1))) = len (n -BinarySequence (i -' 1)) by FINSEQ_5:def 3
.= n by FINSEQ_1:def 18 ;
then reconsider RnB = Rev (n -BinarySequence (i -' 1)) as Tuple of n,BOOLEAN by FINSEQ_2:110;
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 A2;
then A3: RnB in T -level n by TREES_2:def 6;
n -BinarySequence (i -' 1) = Rev RnB by FINSEQ_6:29;
then A4: (NumberOnLevel n,T) . RnB = (Absval (n -BinarySequence (i -' 1))) + 1 by A3, Def1;
A5: RnB in dom (NumberOnLevel n,T) by A3, FUNCT_2:def 1;
i < (2 to_power n) + 1 by A1, NAT_1:13;
then i - 1 < 2 to_power n by XREAL_1:21;
then i -' 1 < 2 to_power n by A1, XREAL_1:235;
then (Absval (n -BinarySequence (i -' 1))) + 1 = (i -' 1) + 1 by BINARI_3:36
.= (i - 1) + 1 by A1, XREAL_1:235
.= i ;
hence (FinSeqLevel n,T) . i = Rev (n -BinarySequence (i -' 1)) by A4, A5, FUNCT_1:54; :: thesis: verum