for i being Nat
for f being FinSequence st len f <= i holds
f /^ i is empty