let f be Function; :: thesis: f is base- f -based
base- f = inf (dom f) by Th007;
hence f is base- f -based by Th003; :: thesis: verum