let T be full Tree; :: thesis: for n being non empty Element of NAT holds len (FinSeqLevel n,T) = 2 to_power n
let n be non empty Element of NAT ; :: thesis: len (FinSeqLevel n,T) = 2 to_power n
rng (FinSeqLevel n,T) = dom (NumberOnLevel n,T) by FUNCT_1:55
.= 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:21
.= 2 to_power n by Th18 ;
hence len (FinSeqLevel n,T) = 2 to_power n by FINSEQ_1:78; :: thesis: verum