:: deftheorem defines commute FUNCT_6:def 10 :
for f being Function holds commute f = curry' (uncurry f);