theorem Th16: :: BINTREE2:16

for T being full Tree
for n being non zero Nat
for y being Element of n -tuples_on BOOLEAN st y = 0* n holds
(FinSeqLevel (n,T)) . (2 to_power n) = 'not' y