let C be Category; :: thesis: for f being Morphism of C holds (id* C) . f = f opp
let f be Morphism of C; :: thesis: (id* C) . f = f opp
thus (id* C) . f = ((id C) . f) opp by Def11
.= f opp by FUNCT_1:18 ; :: thesis: verum