let f be finite Function; :: thesis: ( ( for x being set st x in dom f holds
f . x is finite ) implies product f is finite )
assume for x being set st x in dom f holds
f . x is finite ; :: thesis: product f is finite
then Union f is finite by CARD_2:88;
then Funcs ((dom f),(Union f)) is finite by FRAENKEL:6;
hence product f is finite by FINSET_1:1, FUNCT_6:1; :: thesis: verum