let C be Category; :: thesis: for f, g being Morphism of C st dom g = cod f holds
g (*) f = the Comp of C . (g,f)
let f, g be Morphism of C; :: thesis: ( dom g = cod f implies g (*) f = the Comp of C . (g,f) )
assume dom g = cod f ; :: thesis: g (*) f = the Comp of C . (g,f)
then [g,f] in dom the Comp of C by Def4;
hence g (*) f = the Comp of C . (g,f) by Def1; :: thesis: verum