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

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