theorem Th15: :: FUNCT_5:22

for f, g being Function
for x, y being object st [x,y] in dom f & g = (curry' f) . y holds
( x in dom g & g . x = f . (x,y) )