theorem Th30: :: ISOCAT_2:32

for A, B, C being Category
for F, G being Functor of A,[:B,C:] st Pr1 F = Pr1 G & Pr2 F = Pr2 G holds
F = G by FUNCT_3:80;