let T be full Tree; :: thesis: for n being non zero Nat holds (NumberOnLevel (n,T)) . (0* n) = 1
let n be non zero Nat; :: thesis: (NumberOnLevel (n,T)) . (0* n) = 1
A1: len (Rev (0* n)) = len (0* n) by FINSEQ_5:def 3
.= n by CARD_1:def 7 ;
A2: T = {0,1} * by Def2;
then 0* n is Element of T by BINARI_3:4;
then Rev (0* n) is FinSequence of BOOLEAN by Lm3;
then reconsider F = Rev (0* n) as Element of n -tuples_on BOOLEAN by A1, FINSEQ_2:92;
0* n in T -level n by A2, Th10;
hence (NumberOnLevel (n,T)) . (0* n) = (Absval F) + 1 by Def1
.= 0 + 1 by BINARI_3:6, BINARI_3:8
.= 1 ;
:: thesis: verum