let B, C be Category; :: thesis: for S being Contravariant_Functor of C opp ,B
for c being Object of C holds (/* S) . (id c) = id ((Obj (/* S)) . c)
let S be Contravariant_Functor of C opp ,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)
reconsider i = id c as Morphism of C ;
A1: Hom (c,c) <> {} ;
thus (/* S) . (id c) = S . (i opp) by Def8
.= S . ((id c) opp) by Def6, A1
.= S . (id (c opp)) by Th18
.= id ((Obj S) . (c opp)) by Th29
.= id ((Obj (/* S)) . c) by Th34 ; :: thesis: verum