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