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