for A, B, C, D being category st A,B are_opposite & C,D are_opposite holds
for F, G being covariant Functor of B,C st F,G are_naturally_equivalent holds
((dualizing-func (C,D)) * G) * (dualizing-func (A,B)),((dualizing-func (C,D)) * F) * (dualizing-func (A,B)) are_naturally_equivalent