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