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

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 ) )

hence
*' (*' S) = S
by FUNCT_2:63; :: thesis: verumthus
(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;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