let A, B, C be non empty set ; :: thesis: for f being Function of A,(Funcs B,C) holds curry (uncurry f) = f
let f be Function of A,(Funcs B,C); :: thesis: curry (uncurry f) = f
rng f c= Funcs B,C ;
hence curry (uncurry f) = f by FUNCT_5:55; :: thesis: verum