let T be full Tree; :: thesis: for n being non zero Nat holds rng (FinSeqLevel (n,T)) = T -level n
let n be non zero 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:26;
reconsider dp = dom p as finite set ;
card dp = card (Seg (2 to_power n)) by Th20
.= 2 to_power n by FINSEQ_1:57
.= card Tln by Th18 ;
then p is onto by FINSEQ_4:63;
hence rng (FinSeqLevel (n,T)) = T -level n by FUNCT_2:def 3; :: thesis: verum