let C, B be Category; :: thesis: for S being Functor of C,B
for c being Object of (C opp ) holds (*' S) . (id c) = id ((Obj (*' S)) . c)
let S be Functor of C,B; :: thesis: for c being Object of (C opp ) holds (*' S) . (id c) = id ((Obj (*' S)) . c)
let c be Object of (C opp ); :: thesis: (*' S) . (id c) = id ((Obj (*' S)) . c)
thus (*' S) . (id c) = S . (opp (id c)) by Def8
.= S . (id (opp c))
.= id ((Obj S) . (opp c)) by CAT_1:104
.= id ((Obj (*' S)) . c) by Th41 ; :: thesis: verum