let T be full Tree; :: thesis: for n being non empty Element of NAT holds rng (FinSeqLevel n,T) = T -level n
A1: T = {0 ,1} * by Def2;
let n be non empty Element of NAT ; :: thesis: rng (FinSeqLevel n,T) = T -level n
not T -level n is empty by A1, 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 ;
reconsider Tln = T -level n 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