let B, C be Category; :: thesis: for S being Contravariant_Functor of C,B
for c being Object of (C opp) holds (*' S) . (id c) = id ((Obj S) . (opp c))
let S be Contravariant_Functor of C,B; :: thesis: for c being Object of (C opp) holds (*' S) . (id c) = id ((Obj S) . (opp c))
let c be Object of (C opp); :: thesis: (*' S) . (id c) = id ((Obj S) . (opp c))
thus (*' S) . (id c) = S . (opp (id c)) by Def10
.= S . (id (opp c)) by Th19
.= id ((Obj S) . (opp c)) by Th29 ; :: thesis: verum