for n being Element of NAT
for D being set
for f being FinSequence of D st n in dom f holds
len (f | n) = n