:: deftheorem defines Pr2 ISOCAT_2:def 8 :
for A, B, C being Category
for F being Functor of A,[:B,C:] holds Pr2 F = (pr2 (B,C)) * F;