:: deftheorem defines pr2 CAT_2:def 11 :
for C, D being Category holds pr2 (C,D) = pr2 ( the carrier' of C, the carrier' of D);