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

now :: thesis: ( (*' S) . (id c) = id ((Obj S) . (opp c)) & ( for c being Object of (C opp) ex d being Object of B st (*' S) . (id c) = id d ) )

thus (*' S) . (id c) = id ((Obj S) . (opp c)) by Lm15; :: thesis: for c being Object of (C opp) ex d being Object of B st (*' S) . (id c) = id d
let c be Object of (C opp); :: thesis: ex d being Object of B st (*' S) . (id c) = id d
(*' S) . (id c) = id ((Obj S) . (opp c)) by Lm15;
hence ex d being Object of B st (*' S) . (id c) = id d ; :: thesis: verum

end;

hence (Obj (*' S)) . c = (Obj S) . (opp c) by CAT_1:66; :: thesis: verum