let Fy be finite-yielding Function; :: thesis: ( dom Fy is finite implies union (rng Fy) is finite )
assume dom Fy is finite ; :: thesis: union (rng Fy) is finite
then rng Fy is finite by FINSET_1:8;
hence union (rng Fy) is finite ; :: thesis: verum