for T being full Tree
for n being non zero Nat holds (NumberOnLevel (n,T)) . (0* n) = 1