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