theorem Th10: :: MODCAT_1:10

for R being Ring
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