set d = product f;
let x be set ; :: according to FUNCT_1:def 19 :: thesis: ( not x in product f or x is set )
assume x in product f ; :: thesis: x is set
then ex g being Function st
( x = g & dom g = dom f & ( for x being set st x in dom f holds
g . x in f . x ) ) by Def5;
hence x is set ; :: thesis: verum