theorem Th15: :: BINTREE2:15

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