let T be full Tree; :: thesis: for n being non empty Element of NAT holds rng (FinSeqLevel n,T) = T -level n
let n be non empty Element of NAT ; :: thesis: rng (FinSeqLevel n,T) = T -level n
reconsider Tln = T -level n as finite set ;
T = {0 ,1} * by Def2;
then not T -level n is empty by Th10;
then reconsider p = FinSeqLevel n,T as Function of (dom (FinSeqLevel n,T)),(T -level n) by FINSEQ_2:30;
reconsider dp = dom p as finite set ;
card dp = card (Seg (2 to_power n)) by Th20
.= 2 to_power n by FINSEQ_1:78
.= card Tln by Th18 ;
hence rng (FinSeqLevel n,T) = T -level n by FINSEQ_4:78; :: thesis: verum