theorem Th17: :: BINTREE2:17

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