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:16;
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:15, FUNCT_4:53;
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:16; :: thesis: verum