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 holds (/* (*' S)) . f = S . f

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

end;

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