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