let T be full Tree; :: thesis: for n being non empty Element of NAT holds dom (FinSeqLevel (n,T)) = Seg (2 to_power n)
let n be non empty Element of NAT ; :: thesis: dom (FinSeqLevel (n,T)) = Seg (2 to_power n)
thus dom (FinSeqLevel (n,T)) = Seg (len (FinSeqLevel (n,T))) by FINSEQ_1:def 3
.= Seg (2 to_power n) by Th19 ; :: thesis: verum