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

now :: thesis: for f being Morphism of (C opp) holds (*' S) . f = (S * (*id C)) . f

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

end;

hence *' S = S * (*id C) by FUNCT_2:63; :: thesis: S *' = (id* D) * S

now :: thesis: for f being Morphism of C holds (S *') . f = ((id* D) * S) . f

let f be Morphism of C; :: thesis: (S *') . f = ((id* D) * S) . f
thus (S *') . f = (S . f) opp by Def11
.= (id* D) . (S . f) by Th63
.= ((id* D) * S) . f by FUNCT_2:15 ; :: thesis: verum

end;

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