let E, F, G be non empty set ; :: thesis: for f being Function of [:E,F:],G

for x being object st x in E holds

(curry f) . x is Function of F,G

let f be Function of [:E,F:],G; :: thesis: for x being object st x in E holds

(curry f) . x is Function of F,G

let x be object ; :: thesis: ( x in E implies (curry f) . x is Function of F,G )

assume A1: x in E ; :: thesis: (curry f) . x is Function of F,G

dom f = [:E,F:] by FUNCT_2:def 1;

then consider g being Function such that

A4: ( (curry f) . x = g & dom g = F & rng g c= rng f & ( for y being object st y in F holds

g . y = f . (x,y) ) ) by A1, FUNCT_5:29, ZFMISC_1:90;

thus (curry f) . x is Function of F,G by A4, XBOOLE_1:1, FUNCT_2:2; :: thesis: verum

for x being object st x in E holds

(curry f) . x is Function of F,G

let f be Function of [:E,F:],G; :: thesis: for x being object st x in E holds

(curry f) . x is Function of F,G

let x be object ; :: thesis: ( x in E implies (curry f) . x is Function of F,G )

assume A1: x in E ; :: thesis: (curry f) . x is Function of F,G

dom f = [:E,F:] by FUNCT_2:def 1;

then consider g being Function such that

A4: ( (curry f) . x = g & dom g = F & rng g c= rng f & ( for y being object st y in F holds

g . y = f . (x,y) ) ) by A1, FUNCT_5:29, ZFMISC_1:90;

thus (curry f) . x is Function of F,G by A4, XBOOLE_1:1, FUNCT_2:2; :: thesis: verum