for n being Nat
for f being b₁ -element FinSequence st f is empty holds
n = 0 ;