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