theorem :: RFINSEQ:29

for f being FinSequence
for k being Nat holds len (f /^ k) = (len f) -' k