ex D being non empty set st f is FinSequence of D by Th0;
hence f /^ (len f) is empty by RFINSEQ:27; :: thesis: verum