let C be Category; :: thesis: for g, f being Morphism of C st dom g = cod f holds
g (*) f = the Comp of C . (g,f)
let g, f 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 Def5a;
hence g (*) f = the Comp of C . (g,f) by Def1; :: thesis: verum