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

end;

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