theorem Th13: :: MODCAT_1:15

for UN being Universe
for R being Ring
for f being Morphism of (LModCat (UN,R))
for f9 being Element of Morphs (LModObjects (UN,R)) st f = f9 holds
( dom f = dom f9 & cod f = cod f9 )