theorem Th14: :: BINTREE2:14

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
(NumberOnLevel (n,T)) . ('not' y) = 2 to_power n