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