for n being Element of NAT
for f being FinSequence st len f = 0 holds
f /^ n = f