theorem :: CAT_2:50

for C, D, C9, D9 being Category
for T being Functor of C,D
for T9 being Functor of C9,D9
for c being Object of C
for c9 being Object of C9 holds (Obj [:T,T9:]) . (c,c9) = [((Obj T) . c),((Obj T9) . c9)]