theorem Th29: :: ISOCAT_2:31

for A, B, C being Category
for F being Functor of A,B
for G being Functor of A,C holds
( Pr1 <:F,G:> = F & Pr2 <:F,G:> = G ) by FUNCT_3:62;