let C, D be Category; :: thesis: for S being Function of the carrier' of (C opp), the carrier' of D holds *' (/* S) = S
let S be Function of the carrier' of (C opp), 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) . (opp f) by Def10
.= S . ((opp f) opp) by Def8
.= S . f ; :: thesis: verum

end;

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