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