let B, C be Category; :: thesis: for S being Contravariant_Functor of C,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,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 Th43
.= (dom (S . f)) opp by Th30
.= cod ((S . f) opp) ;
(Obj (S *')) . (dom f) = ((Obj S) . (dom f)) opp by Th43
.= (cod (S . f)) opp by Th30
.= dom ((S . f) opp) ;
hence ( (Obj (S *')) . (dom f) = dom ((S *') . f) & (Obj (S *')) . (cod f) = cod ((S *') . f) ) by A1, Def11; :: thesis: verum