theorem Th17: :: FUNCT_5:24

for X, Y being set
for f being Function st [:X,Y:] <> {} & dom f = [:X,Y:] holds
( dom (curry f) = X & dom (curry' f) = Y )