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 holds ((*' F) *') . (f opp) = (F . f) opp

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

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

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

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

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

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

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

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

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