A1: ( ( for f, g, h being Morphism of (LModCat (UN,R)) st dom h = cod g & dom g = cod f holds
h * (g * f) = (h * g) * f ) & ( for b being Object of (LModCat (UN,R)) holds
( dom (id b) = b & cod (id b) = b & ( for f being Morphism of (LModCat (UN,R)) st cod f = b holds
(id b) * f = f ) & ( for g being Morphism of (LModCat (UN,R)) st dom g = b holds
g * (id b) = g ) ) ) ) by Lm2, Lm3;
( ( 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 ) ) & ( for f, g being Morphism of (LModCat (UN,R)) st dom g = cod f holds
( dom (g * f) = dom f & cod (g * f) = cod g ) ) ) by Lm1, Th14;
hence LModCat (UN,R) is Category-like by A1, CAT_1:10; :: thesis: verum