:: deftheorem defines uncurry' FUNCT_5:def 4 :
for f being Function holds uncurry' f = ~ (uncurry f);