theorem Th14: :: MODCAT_1:16

for UN being Universe
for R being Ring
for f, g being Morphism of (LModCat (UN,R))
for f9, g9 being Element of Morphs (LModObjects (UN,R)) st f = f9 & g = g9 holds
( ( dom g = cod f implies dom g9 = cod f9 ) & ( dom g9 = cod f9 implies dom g = cod f ) & ( dom g = cod f implies [g9,f9] in dom (comp (LModObjects (UN,R))) ) & ( [g9,f9] in dom (comp (LModObjects (UN,R))) implies dom g = cod f ) & ( dom g = cod f implies g (*) f = g9 * f9 ) & ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) )