theorem Th26: :: FUNCT_6:31

for x being object
for g being Function
for f being Function-yielding Function st x in dom <:f:> & g = <:f:> . x holds
( dom g = dom f & ( for y being object st y in dom g holds
( [y,x] in dom (uncurry f) & g . y = (uncurry f) . (y,x) ) ) )