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 )

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

hence
*' S = S * (*id C)
by FUNCT_2:63; :: thesis: S *' = (id* D) * Slet 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;thus (*' S) . f = S . (opp f) by Def10

.= S . ((*id C) . f) by Th65

.= (S * (*id C)) . f by FUNCT_2:15 ; :: thesis: verum

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

hence
S *' = (id* D) * S
by FUNCT_2:63; :: thesis: verumlet 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;thus (S *') . f = (S . f) opp by Def11

.= (id* D) . (S . f) by Th63

.= ((id* D) * S) . f by FUNCT_2:15 ; :: thesis: verum