let B, C be Category; :: thesis: for S being Function of the carrier' of (C opp), the carrier' of B

for f being Morphism of (C opp) holds (/* S) . (opp f) = S . f

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

let f be Morphism of (C opp); :: thesis: (/* S) . (opp f) = S . f

thus (/* S) . (opp f) = S . ((opp f) opp) by Def8

.= S . f ; :: thesis: verum

for f being Morphism of (C opp) holds (/* S) . (opp f) = S . f

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

let f be Morphism of (C opp); :: thesis: (/* S) . (opp f) = S . f

thus (/* S) . (opp f) = S . ((opp f) opp) by Def8

.= S . f ; :: thesis: verum