let C, D be Category; :: thesis: for F being Function of the carrier' of C, the carrier' of D

for f being Morphism of (C opp) holds ((*' F) *') . f = (F . (opp f)) opp

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

let f be Morphism of (C opp); :: thesis: ((*' F) *') . f = (F . (opp f)) opp

thus ((*' F) *') . f = ((*' F) . f) opp by Def11

.= (F . (opp f)) opp by Def10 ; :: thesis: verum

for f being Morphism of (C opp) holds ((*' F) *') . f = (F . (opp f)) opp

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

let f be Morphism of (C opp); :: thesis: ((*' F) *') . f = (F . (opp f)) opp

thus ((*' F) *') . f = ((*' F) . f) opp by Def11

.= (F . (opp f)) opp by Def10 ; :: thesis: verum