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 Th41
.= opp c by CAT_1:116 ; :: thesis: verum