let C be Category; :: thesis: for c being Object of (C opp) holds (Obj (*id C)) . c = opp c
let c be Object of (C opp); :: thesis: (Obj (*id C)) . c = opp c
thus (Obj (*id C)) . c = (Obj (id C)) . (opp c) by Th38
.= opp c by CAT_1:77 ; :: thesis: verum