theorem Th13: :: BINTREE2:13
for T being full Tree
for n being non zero Nat holds (NumberOnLevel (n,T)) . (0* n) = 1