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 Def8;
hence g * f = the Comp of C . g,f by Def4; :: thesis: verum