let C, B be Category; :: thesis: for S being Contravariant_Functor of C opp ,B
for c being Object of (C opp ) holds (Obj (/* S)) . (opp c) = (Obj S) . c
let S be Contravariant_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 Th37
.= (Obj S) . c ; :: thesis: verum