theorem Th22: :: FUNCT_5:29

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