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