let x be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in proj1 (curry f) or (curry f) . x is set )
assume x in dom (curry f) ; :: thesis: (curry f) . x is set
then A1: x in proj1 (dom f) by Def1;
ex g being Function st
( (curry f) . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being object st y in dom g holds
g . y = f . (x,y) ) ) by A1, Def1;
hence (curry f) . x is set ; :: thesis: verum