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 & B <> {} ) ;
hence curry (uncurry f) = f by FUNCT_5:55; :: thesis: verum