for f being non-decreasing Ordinal-Sequence st not dom f is empty holds
Union f is_limes_of f