let x be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in proj1 (Frege f) or (Frege f) . x is set )
assume A1: x in dom (Frege f) ; :: thesis: (Frege f) . x is set
then A2: x in product (doms f) by FUNCT_6:def 7;
reconsider x = x as Element of product (doms f) by A1, FUNCT_6:def 7;
consider h being Function such that
A3: ( (Frege f) . x = h & dom h = dom f & ( for y being object st y in dom h holds
h . y = (uncurry f) . (y,(x . y)) ) ) by A2, FUNCT_6:def 7;
thus (Frege f) . x is set by A3; :: thesis: verum