for D being non empty set
for f being FinSequence of D
for k being Nat holds len (f /^ k) = (len f) -' k by RFINSEQ:29;