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 :: thesis: for f being Morphism of (C opp) holds ((*' S) *') . f = (*' (S *')) . f

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

end;

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