let T be full Tree; :: thesis: for n being non zero Nat holds dom (FinSeqLevel (n,T)) = Seg (2 to_power n)
let n be non zero 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