theorem Th31: :: FUNCT_5:38

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