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

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

end;

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