for C1, C2 being category holds C1 [x] C2, pr1 (C1,C2), pr2 (C1,C2) is_product_of C1,C2