let C, B be Category; :: thesis: for S being Contravariant_Functor of C opp ,B
for f being Morphism of C holds
( (Obj (/* S)) . (dom f) = dom ((/* S) . f) & (Obj (/* S)) . (cod f) = cod ((/* S) . f) )
let S be Contravariant_Functor of C opp ,B; :: thesis: for f being Morphism of C holds
( (Obj (/* S)) . (dom f) = dom ((/* S) . f) & (Obj (/* S)) . (cod f) = cod ((/* S) . f) )
let f be Morphism of C; :: thesis: ( (Obj (/* S)) . (dom f) = dom ((/* S) . f) & (Obj (/* S)) . (cod f) = cod ((/* S) . f) )

now

thus (Obj (/* S)) . (dom f) = (Obj S) . ((dom f) opp ) by Th37
.= (Obj S) . (cod (f opp ))
.= dom (S . (f opp )) by Th33 ; :: thesis: (Obj (/* S)) . (cod f) = cod (S . (f opp ))
thus (Obj (/* S)) . (cod f) = (Obj S) . ((cod f) opp ) by Th37
.= (Obj S) . (dom (f opp ))
.= cod (S . (f opp )) by Th33 ; :: thesis: verum

end;

hence ( (Obj (/* S)) . (dom f) = dom ((/* S) . f) & (Obj (/* S)) . (cod f) = cod ((/* S) . f) ) by Def6; :: thesis: verum