let B, C 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) )
A1: (Obj (/* S)) . (cod f) = (Obj S) . ((cod f) opp) by Th34
.= (Obj S) . (dom (f opp))
.= cod (S . (f opp)) by Th30 ;
(Obj (/* S)) . (dom f) = (Obj S) . ((dom f) opp) by Th34
.= (Obj S) . (cod (f opp))
.= dom (S . (f opp)) by Th30 ;
hence ( (Obj (/* S)) . (dom f) = dom ((/* S) . f) & (Obj (/* S)) . (cod f) = cod ((/* S) . f) ) by A1, Def8; :: thesis: verum