let B, C be Category; :: thesis: for S being Function of the carrier' of C, the carrier' of B
for f being Morphism of C holds (*' S) . (f opp) = S . f
let S be Function of the carrier' of C, the carrier' of B; :: thesis: for f being Morphism of C holds (*' S) . (f opp) = S . f
let f be Morphism of C; :: thesis: (*' S) . (f opp) = S . f
thus (*' S) . (f opp) = S . (opp (f opp)) by Def10
.= S . f ; :: thesis: verum