A1: rng f c= Funcs B,C ;
then A2: dom (uncurry f) = [:(dom f),B:] by FUNCT_5:33
.= [:A,B:] by FUNCT_2:def 1 ;
rng (uncurry f) c= C by A1, FUNCT_5:48;
hence uncurry f is Function of [:A,B:],C by A2, FUNCT_2:def 1, RELSET_1:11; :: thesis: verum