let R be Ring; :: thesis: for V being LeftMod_DOMAIN of R
for g, f being Element of Morphs V st dom g = cod f holds
g * f in Morphs V
let V be LeftMod_DOMAIN of R; :: thesis: for g, f being Element of Morphs V st dom g = cod f holds
g * f in Morphs V
let g, f be Element of Morphs V; :: thesis: ( dom g = cod f implies g * f in Morphs V )
assume dom g = cod f ; :: thesis: g * f in Morphs V
then dom' g = cod' f ;
hence g * f in Morphs V by Th9; :: thesis: verum