let C, D be Category; :: thesis: for S being Function of the carrier' of C,the carrier' of D holds (*' S) *' = *' (S *' )
let S be Function of the carrier' of C,the carrier' of D; :: thesis: (*' S) *' = *' (S *' )

now

let f be Morphism of (C opp ); :: thesis: ((*' S) *' ) . f = (*' (S *' )) . f
thus ((*' S) *' ) . f = ((*' S) . f) opp by Def9
.= (S . (opp f)) opp by Def8
.= (S *' ) . (opp f) by Def9
.= (*' (S *' )) . f by Def8 ; :: thesis: verum

end;

hence (*' S) *' = *' (S *' ) by FUNCT_2:113; :: thesis: verum