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