theorem :: RFINSEQ:27

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