let C be Category; :: thesis: for f, g being Morphism of C st dom g = cod f holds
( dom (g * f) = dom f & cod (g * f) = cod g )
let f, g be Morphism of C; :: thesis: ( dom g = cod f implies ( dom (g * f) = dom f & cod (g * f) = cod g ) )
assume A1: dom g = cod f ; :: thesis: ( dom (g * f) = dom f & cod (g * f) = cod g )
then the Comp of C . (g,f) = g * f by Th41;
hence ( dom (g * f) = dom f & cod (g * f) = cod g ) by A1, Def8; :: thesis: verum