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 :: thesis: ( (C opp) opp = C & ( for f being Morphism of ((C opp) opp) holds (*' (*' S)) . f = S . f ) )

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

end;

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