Funcs ((dom f),(Union f)) is finite by FRAENKEL:6;
hence product f is finite by FINSET_1:1, FUNCT_6:1; :: thesis: verum