theorem :: BINTREE2:24

for T being full Tree
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)*>