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

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