( ( for f, g being Morphism of (RingCat UN) holds
( [g,f] in dom the Comp of (RingCat UN) iff dom g = cod f ) ) & ( for f, g being Morphism of (RingCat UN) st dom g = cod f holds
( dom (g * f) = dom f & cod (g * f) = cod g ) ) & ( for f, g, h being Morphism of (RingCat UN) st dom h = cod g & dom g = cod f holds
h * (g * f) = (h * g) * f ) & ( for b being Object of (RingCat UN) holds
( dom (id b) = b & cod (id b) = b & ( for f being Morphism of (RingCat UN) st cod f = b holds
(id b) * f = f ) & ( for g being Morphism of (RingCat UN) st dom g = b holds
g * (id b) = g ) ) ) ) by Lm9, Lm10, Lm11, Th26;
hence RingCat UN is Category-like by CAT_1:29; :: thesis: verum