let C, D be Category; :: thesis: for F being Function of the carrier' of C,the carrier' of D
for f being Morphism of (C opp ) holds ((*' F) *' ) . f = (F . (opp f)) opp
let F be Function of the carrier' of C,the carrier' of D; :: thesis: for f being Morphism of (C opp ) holds ((*' F) *' ) . f = (F . (opp f)) opp
let f be Morphism of (C opp ); :: thesis: ((*' F) *' ) . f = (F . (opp f)) opp
thus ((*' F) *' ) . f = ((*' F) . f) opp by Def9
.= (F . (opp f)) opp by Def8 ; :: thesis: verum