for p being FinTree-yielding FinSequence
for n being empty Element of tree p holds card (succ n) = len p