theorem Th21: :: CATALG_1:21
for C1, C2 being Category
for F being Functor of C1,C2
for a, b being Object of C1 holds (Upsilon F) . (homsym (a,b)) = homsym ((F . a),(F . b))