for Fy being finite-yielding Function st dom Fy is finite holds
union (rng Fy) is finite