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

now

thus (Obj (*' S)) . (dom f) = (Obj S) . (opp (dom f)) by Th41
.= (Obj S) . (cod (opp f))
.= cod (S . (opp f)) by CAT_1:105 ; :: thesis: (Obj (*' S)) . (cod f) = dom (S . (opp f))
thus (Obj (*' S)) . (cod f) = (Obj S) . (opp (cod f)) by Th41
.= (Obj S) . (dom (opp f))
.= dom (S . (opp f)) by CAT_1:105 ; :: thesis: verum

end;

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