theorem Th13: :: FUNCT_5:20
for f, g being Function
for x, y being object st [x,y] in dom f & g = (curry f) . x holds
( y in dom g & g . y = f . (x,y) )