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