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