let C be Category; :: thesis: for a, b, c being Object of C
for f being Morphism of a,b
for g being Morphism of b,c st Hom a,b <> {} & Hom b,c <> {} holds
(g * f) opp = (f opp ) * (g opp )
let a, b, c be Object of C; :: thesis: for f being Morphism of a,b
for g being Morphism of b,c st Hom a,b <> {} & Hom b,c <> {} holds
(g * f) opp = (f opp ) * (g opp )
let f be Morphism of a,b; :: thesis: for g being Morphism of b,c st Hom a,b <> {} & Hom b,c <> {} holds
(g * f) opp = (f opp ) * (g opp )
let g be Morphism of b,c; :: thesis: ( Hom a,b <> {} & Hom b,c <> {} implies (g * f) opp = (f opp ) * (g opp ) )
assume A1: ( Hom a,b <> {} & Hom b,c <> {} ) ; :: thesis: (g * f) opp = (f opp ) * (g opp )
then A2: g * f = g * f by CAT_1:def 13;
( cod f = b & dom g = b ) by A1, CAT_1:23;
hence (g * f) opp = (f opp ) * (g opp ) by A2, Th17; :: thesis: verum