theorem Th30: :: OPPCAT_1:32

for C, D being Category
for S being Contravariant_Functor of C,D
for f being Morphism of C holds
( (Obj S) . (dom f) = cod (S . f) & (Obj S) . (cod f) = dom (S . f) )