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

A1: now :: thesis: for c being Object of C ex d being Object of B st (/* S) . (id c) = id d

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

end;

(/* S) . (id c) = id ((Obj S) . (c opp)) by Lm4;
hence (Obj (/* S)) . c = (Obj S) . (c opp) by A1, CAT_1:66; :: thesis: verum