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

for y being object st y in F holds

(curry' f) . y is Function of E,G

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

(curry' f) . y is Function of E,G

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

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

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

then ex g being Function st

( (curry' f) . y = g & dom g = E & rng g c= rng f & ( for x being object st x in E holds

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

hence (curry' f) . y is Function of E,G by XBOOLE_1:1, FUNCT_2:2; :: thesis: verum

for y being object st y in F holds

(curry' f) . y is Function of E,G

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

(curry' f) . y is Function of E,G

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

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

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

then ex g being Function st

( (curry' f) . y = g & dom g = E & rng g c= rng f & ( for x being object st x in E holds

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

hence (curry' f) . y is Function of E,G by XBOOLE_1:1, FUNCT_2:2; :: thesis: verum