let T be full Tree; :: thesis: for n, i being non zero Nat st i <= 2 to_power (n + 1) holds
for F being Element of n -tuples_on BOOLEAN st F = (FinSeqLevel (n,T)) . ((i + 1) div 2) holds
(FinSeqLevel ((n + 1),T)) . i = F ^ <*((i + 1) mod 2)*>
let n, i be non zero Nat; :: thesis: ( i <= 2 to_power (n + 1) implies for F being Element of n -tuples_on BOOLEAN st F = (FinSeqLevel (n,T)) . ((i + 1) div 2) holds
(FinSeqLevel ((n + 1),T)) . i = F ^ <*((i + 1) mod 2)*> )
assume A1: i <= 2 to_power (n + 1) ; :: thesis: for F being Element of n -tuples_on BOOLEAN st F = (FinSeqLevel (n,T)) . ((i + 1) div 2) holds
(FinSeqLevel ((n + 1),T)) . i = F ^ <*((i + 1) mod 2)*>

A2: now :: thesis: (i + 1) mod 2 = (i -' 1) mod 2

per cases ( i -' 1 is odd or i -' 1 is even ) ;

suppose i -' 1 is odd ; :: thesis: (i + 1) mod 2 = (i -' 1) mod 2

then A3: (i -' 1) mod 2 = 1 by NAT_2:22;
then ((i -' 1) + ((1 + 1) * 1)) mod 2 = 1 by NAT_D:21;
then (((i -' 1) + 1) + 1) mod 2 = 1 ;
hence (i + 1) mod 2 = (i -' 1) mod 2 by A3, NAT_1:14, XREAL_1:235; :: thesis: verum

end;

suppose i -' 1 is even ; :: thesis: (i + 1) mod 2 = (i -' 1) mod 2

then A4: (i -' 1) mod 2 = 0 by NAT_2:21;
then ((i -' 1) + ((1 + 1) * 1)) mod 2 = 0 by NAT_D:21;
then (((i -' 1) + 1) + 1) mod 2 = 0 ;
hence (i + 1) mod 2 = (i -' 1) mod 2 by A4, NAT_1:14, XREAL_1:235; :: thesis: verum

end;

end;

end;

let F be Element of n -tuples_on BOOLEAN; :: thesis: ( F = (FinSeqLevel (n,T)) . ((i + 1) div 2) implies (FinSeqLevel ((n + 1),T)) . i = F ^ <*((i + 1) mod 2)*> )
assume A5: F = (FinSeqLevel (n,T)) . ((i + 1) div 2) ; :: thesis: (FinSeqLevel ((n + 1),T)) . i = F ^ <*((i + 1) mod 2)*>
A6: 1 <= i by NAT_1:14;
then 1 + 1 <= i + 1 by XREAL_1:6;
then A7: 1 <= (i + 1) div 2 by NAT_2:13;
2 to_power (n + 1) = (2 to_power n) * (2 to_power 1) by POWER:27
.= 2 * (2 to_power n) by POWER:25 ;
then (i + 1) div 2 <= 2 to_power n by A1, NAT_2:25;
then A8: (i + 1) div 2 in Seg (2 to_power n) by A7, FINSEQ_1:1;
i + 1 >= 1 + 1 by A6, XREAL_1:6;
then A9: 1 <= (i + 1) div 2 by NAT_2:13;
A10: (i -' 1) div 2 = (((i -' 1) div 2) + 1) - 1
.= (((i -' 1) + (1 + 1)) div 2) - 1 by NAT_2:14
.= ((((i -' 1) + 1) + 1) div 2) - 1
.= ((i + 1) div 2) - 1 by NAT_1:14, XREAL_1:235
.= ((i + 1) div 2) -' 1 by A9, XREAL_1:233 ;
i in Seg (2 to_power (n + 1)) by A1, A6, FINSEQ_1:1;
hence (FinSeqLevel ((n + 1),T)) . i = Rev ((n + 1) -BinarySequence (i -' 1)) by Th17
.= Rev (<*((i -' 1) mod 2)*> ^ (n -BinarySequence ((i -' 1) div 2))) by BINARI_3:34
.= (Rev (n -BinarySequence (((i + 1) div 2) -' 1))) ^ <*((i + 1) mod 2)*> by A2, A10, FINSEQ_6:24
.= F ^ <*((i + 1) mod 2)*> by A5, A8, Th17 ;
:: thesis: verum