theorem Th20: :: BINTREE2:20

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