the carrier' of [:A,B:] = [:the carrier' of A,the carrier' of B:] by CAT_2:33;
then reconsider F = F as Function of [:the carrier' of A,the carrier' of B:],the carrier' of C ;
(curry F) . f is Function of the carrier' of B,the carrier' of C ;
hence (curry F) . f is Function of the carrier' of B,the carrier' of C ; :: thesis: verum