[: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 CAT_2:1;
hence (curry f) . x is Function of X2,Y by FUNCT_2:7, FUNCT_2:121; :: thesis: verum