thus f /^ (len f) is empty by RFINSEQ:27; :: thesis: verum