theorem :: FINSEQ_6:167

for D being non empty set
for f being FinSequence of D holds f /^ (len f) = {} by RFINSEQ:27;