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 Def8
.= opp f by FUNCT_1:35 ; :: thesis: verum