:: deftheorem Def1 defines curry FUNCT_5:def 1 :
for f, b₂ being Function holds
( b₂ = curry f iff ( dom b₂ = proj1 (dom f) & ( for x being object st x in proj1 (dom f) holds
ex g being Function st
( b₂ . 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) ) ) ) ) );