let E, F, G be non empty set ; :: thesis: for f being Function of [:E,F:],G
for x, y being object st x in E & y in F holds
((curry f) . x) . y = f . (x,y)
let f be Function of [:E,F:],G; :: thesis: for x, y being object st x in E & y in F holds
((curry f) . x) . y = f . (x,y)
let x, y be object ; :: thesis: ( x in E & y in F implies ((curry f) . x) . y = f . (x,y) )
assume that
A1: x in E and
A2: y in F ; :: thesis: ((curry f) . x) . y = f . (x,y)
dom f = [:E,F:] by FUNCT_2:def 1;
then ex g being Function st
( (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;
hence ((curry f) . x) . y = f . (x,y) by A2; :: thesis: verum