let T be full Tree; :: thesis: for n being non empty Element of NAT holds (NumberOnLevel n,T) . (0* n) = 1
A1: T = {0 ,1} * by Def2;
let n be non empty Element of NAT ; :: thesis: (NumberOnLevel n,T) . (0* n) = 1
A2: 0* n is Element of T by A1, BINARI_3:5;
A3: 0* n in T -level n by A1, Th10;
A4: Rev (0* n) is FinSequence of BOOLEAN by A2, Lm3;
len (Rev (0* n)) = len (0* n) by FINSEQ_5:def 3
.= n by FINSEQ_1:def 18 ;
then reconsider F = Rev (0* n) as Tuple of n,BOOLEAN by A4, FINSEQ_2:110;
thus (NumberOnLevel n,T) . (0* n) = (Absval F) + 1 by A3, Def1
.= 0 + 1 by BINARI_3:7, BINARI_3:9
.= 1 ; :: thesis: verum