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) )
A1: (Obj (/* S)) . (cod f) = (Obj S) . ((cod f) opp) by Th37
.= (Obj S) . (dom (f opp))
.= cod (S . (f opp)) by Th33 ;
(Obj (/* S)) . (dom f) = (Obj S) . ((dom f) opp) by Th37
.= (Obj S) . (cod (f opp))
.= dom (S . (f opp)) by Th33 ;
hence ( (Obj (/* S)) . (dom f) = dom ((/* S) . f) & (Obj (/* S)) . (cod f) = cod ((/* S) . f) ) by A1, Def6; :: thesis: verum