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