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