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 A1: rng Fy is finite by FINSET_1:26;
for F being set st F in rng Fy holds
F is finite

proof

let F be set ; :: thesis: ( F in rng Fy implies F is finite )
assume A2: F in rng Fy ; :: thesis: F is finite
ex x being set st
( x in dom Fy & F = Fy . x ) by A2, FUNCT_1:def 5;
hence F is finite ; :: thesis: verum

end;

hence union (rng Fy) is finite by A1, FINSET_1:25; :: thesis: verum