let f be Function; :: thesis: f is limit- f -limited
limit- f = sup (dom f) by Th16;
hence f is limit- f -limited by Def3; :: thesis: verum