let T be full Tree; :: thesis: for n being non zero Nat holds len (FinSeqLevel (n,T)) = 2 to_power n
let n be non zero Nat; :: thesis: len (FinSeqLevel (n,T)) = 2 to_power n
rng (FinSeqLevel (n,T)) = dom (NumberOnLevel (n,T)) by FUNCT_1:33
.= T -level n by FUNCT_2:def 1 ;
then A1: dom (FinSeqLevel (n,T)),T -level n are_equipotent by WELLORD2:def 4;
card (Seg (len (FinSeqLevel (n,T)))) = card (dom (FinSeqLevel (n,T))) by FINSEQ_1:def 3
.= card (T -level n) by A1, CARD_1:5
.= 2 to_power n by Th18 ;
hence len (FinSeqLevel (n,T)) = 2 to_power n by FINSEQ_1:57; :: thesis: verum