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