let B, C be Category; :: thesis: for S being Contravariant_Functor of C,B
for f being Morphism of (C opp) holds
( (Obj (*' S)) . (dom f) = dom ((*' S) . f) & (Obj (*' S)) . (cod f) = cod ((*' S) . f) )
let S be Contravariant_Functor of C,B; :: thesis: for f being Morphism of (C opp) holds
( (Obj (*' S)) . (dom f) = dom ((*' S) . f) & (Obj (*' S)) . (cod f) = cod ((*' S) . f) )
let f be Morphism of (C opp); :: thesis: ( (Obj (*' S)) . (dom f) = dom ((*' S) . f) & (Obj (*' S)) . (cod f) = cod ((*' S) . f) )
A1: (Obj (*' S)) . (cod f) = (Obj S) . (opp (cod f)) by Th41
.= (Obj S) . (dom (opp f))
.= cod (S . (opp f)) by Th30 ;
(Obj (*' S)) . (dom f) = (Obj S) . (opp (dom f)) by Th41
.= (Obj S) . (cod (opp f))
.= dom (S . (opp f)) by Th30 ;
hence ( (Obj (*' S)) . (dom f) = dom ((*' S) . f) & (Obj (*' S)) . (cod f) = cod ((*' S) . f) ) by A1, Def10; :: thesis: verum