theorem Th23: :: CATALG_1:23

for C1, C2 being Category
for F being Functor of C1,C2
for a, b, c being Object of C1 holds (Psi F) . (compsym (a,b,c)) = compsym ((F . a),(F . b),(F . c))