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

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

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

end;

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