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:63; :: thesis: verum