theorem :: FUNCT_5:34

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