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