theorem :: BINTREE2:21

for T being full Tree
for n being non zero Nat holds rng (FinSeqLevel (n,T)) = T -level n