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 ;

hence rng (FinSeqLevel (n,T)) = T -level n by FINSEQ_4:63; :: thesis: verum

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 ;

hence rng (FinSeqLevel (n,T)) = T -level n by FINSEQ_4:63; :: thesis: verum