[: the carrier of X1, the carrier of X2:] = the carrier of [:X1,X2:] by YELLOW_3:def 2;
then curry' f is Function of the carrier of X2,(Funcs ( the carrier of X1, the carrier of Y)) by FUNCT_5:68;
hence (curry' f) . y is Function of X1,Y by FUNCT_2:5, FUNCT_2:66; :: thesis: verum