let C be Category; :: thesis: for f, g being Morphism of C st cod (g opp) = dom (f opp) holds
(g * f) opp = (f opp) * (g opp)
let f, g be Morphism of C; :: thesis: ( cod (g opp) = dom (f opp) implies (g * f) opp = (f opp) * (g opp) )
( cod (g opp) = dom g & dom (f opp) = cod f ) ;
hence ( cod (g opp) = dom (f opp) implies (g * f) opp = (f opp) * (g opp) ) by Th17; :: thesis: verum