theorem Th24: :: FUNCT_5:31

for x being object
for f, g being Function st x in dom (curry f) & g = (curry f) . x holds
( dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & dom g c= proj2 (dom f) & rng g c= rng f & ( for y being object st y in dom g holds
( g . y = f . (x,y) & [x,y] in dom f ) ) )