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_3:134;
then Funcs ((dom f),(Union f)) is finite by FRAENKEL:16;
hence product f is finite by FINSET_1:13, FUNCT_6:10; :: thesis: verum