theorem Th25: :: FUNCT_5:32

for X, Y being set
for y being object
for f being Function st [:X,Y:] <> {} & dom f = [:X,Y:] & y in Y holds
ex g being Function st
( (curry' f) . y = g & dom g = X & rng g c= rng f & ( for x being object st x in X holds
g . x = f . (x,y) ) )