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