:: deftheorem defines Pr2 ISOCAT_2:def 10 :
for A, B, C being Category
for F1, F2 being Functor of A,[:B,C:]
for t being natural_transformation of F1,F2 holds Pr2 t = (pr2 (B,C)) * t;