let C, B 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) )

now

thus (Obj (S *' )) . (dom f) = ((Obj S) . (dom f)) opp by Th46
.= (cod (S . f)) opp by Th33
.= dom ((S . f) opp ) ; :: thesis: (Obj (S *' )) . (cod f) = cod ((S . f) opp )
thus (Obj (S *' )) . (cod f) = ((Obj S) . (cod f)) opp by Th46
.= (dom (S . f)) opp by Th33
.= cod ((S . f) opp ) ; :: thesis: verum

end;

hence ( (Obj (S *' )) . (dom f) = dom ((S *' ) . f) & (Obj (S *' )) . (cod f) = cod ((S *' ) . f) ) by Def9; :: thesis: verum