for D being non empty set
for f being FinSequence of D
for n, m being Element of NAT st n <= m holds
len (f /^ m) <= len (f /^ n)