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

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

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