theorem :: RFINSEQ:27

for f being FinSequence holds f /^ (len f) = {}