[: 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 X1,(Funcs ( the carrier of X2, the carrier of Y)) by FUNCT_5:67;
hence (curry f) . x is Function of X2,Y by FUNCT_2:5, FUNCT_2:66; :: thesis: verum