thus lim f is empty by Def1; :: thesis: verum