theorem Th12: :: MODCAT_1:12

for UN being Universe
for R being Ring
for f, g being Morphism of (LModCat (UN,R)) holds
( [g,f] in dom the Comp of (LModCat (UN,R)) iff dom g = cod f )