let C be Category; :: thesis: for f, g being Morphism of C st dom g = cod f holds
(g * f) opp = (f opp ) * (g opp )
let f, g be Morphism of C; :: thesis: ( dom g = cod f implies (g * f) opp = (f opp ) * (g opp ) )
assume A1: dom g = cod f ; :: thesis: (g * f) opp = (f opp ) * (g opp )
then A2: g * f = the Comp of C . g,f by CAT_1:41;
A3: ( dom g = cod (g opp ) & cod f = dom (f opp ) ) ;
then ( the Comp of C = ~ the Comp of (C opp ) & [(f opp ),(g opp )] in dom the Comp of (C opp ) ) by A1, CAT_1:40, FUNCT_4:54;
then the Comp of C . g,f = the Comp of (C opp ) . (f opp ),(g opp ) by FUNCT_4:def 2;
hence (g * f) opp = (f opp ) * (g opp ) by A1, A2, A3, CAT_1:41; :: thesis: verum