let B, C be Category; :: thesis: for S being Functor of C,B
for c being Object of C holds (S *') . (id c) = id (((Obj S) . c) opp)
let S be Functor of C,B; :: thesis: for c being Object of C holds (S *') . (id c) = id (((Obj S) . c) opp)
let c be Object of C; :: thesis: (S *') . (id c) = id (((Obj S) . c) opp)
A1: Hom (((Obj S) . c),((Obj S) . c)) <> {} ;
thus (S *') . (id c) = (S . (id c)) opp by Def11
.= (id ((Obj S) . c)) opp by CAT_1:68
.= (id ((Obj S) . c)) opp by Def6, A1
.= id (((Obj S) . c) opp) by Th18 ; :: thesis: verum