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 *')

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

hence
(*' S) *' = *' (S *')
by FUNCT_2:63; :: thesis: verumlet 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;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