theorem Th19: :: BINTREE2:19

for T being full Tree
for n being non zero Nat holds len (FinSeqLevel (n,T)) = 2 to_power n