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

thus (D opp) opp = D by FUNCT_4:53; :: 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 Def11
.= ((S . f) opp) opp by Def11
.= S . f ; :: thesis: verum

end;

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