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