let E, F, G be non empty set ; for f being Function of [:E,F:],G
for x, y being object st x in E & y in F holds
((curry' f) . y) . x = f . (x,y)
let f be Function of [:E,F:],G; for x, y being object st x in E & y in F holds
((curry' f) . y) . x = f . (x,y)
let x, y be object ; ( x in E & y in F implies ((curry' f) . y) . x = f . (x,y) )
assume that
A1:
x in E
and
A2:
y in F
; ((curry' f) . y) . x = f . (x,y)
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 A2, FUNCT_5:32, ZFMISC_1:90;
hence
((curry' f) . y) . x = f . (x,y)
by A1; verum