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 Th41; :: thesis: verum