let T be full Tree; for n being non empty Element of NAT holds (NumberOnLevel (n,T)) . (0* n) = 1
let n be non empty Element of NAT ; (NumberOnLevel (n,T)) . (0* n) = 1
A1: len (Rev (0* n)) =
len (0* n)
by FINSEQ_5:def 3
.=
n
by FINSEQ_1:def 18
;
A2:
T = {0,1} *
by Def2;
then
0* n is Element of T
by BINARI_3:5;
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:110;
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:7, BINARI_3:9
.=
1
;
verum