let f be Morphism of (RingCat UN); :: according to CAT_1:def 6 :: thesis:
thus for b₁ being Element of the carrier' of (RingCat UN) holds
( ( not [b₁,f] in proj1 the Comp of (RingCat UN) or dom b₁ = cod f ) & ( not dom b₁ = cod f or [b₁,f] in proj1 the Comp of (RingCat UN) ) ) by Th21; :: thesis:

end;

let f be Morphism of (RingCat UN); :: according to CAT_1:def 7 :: thesis:
thus for b₁ being Element of the carrier' of (RingCat UN) holds
( not dom b₁ = cod f or ( dom (b₁ (*) f) = dom f & cod (b₁ (*) f) = cod b₁ ) ) by Lm9; :: thesis:

end;

let f be Morphism of (RingCat UN); :: according to CAT_1:def 8 :: thesis:
thus for b₁, b₂ being Element of the carrier' of (RingCat UN) holds
( not dom b₂ = cod b₁ or not dom b₁ = cod f or b₂ (*) (b₁ (*) f) = (b₂ (*) b₁) (*) f ) by Lm10; :: thesis:

end;

let a be Element of (RingCat UN); :: according to CAT_1:def 9 :: thesis:
reconsider G = a as Element of RingObjects UN ;
consider x being set such that
x in UN and
W2: GO x,G by Def16;
set ii = ID G;
consider x1, x2, x3, x4, x5, x6 being set such that
x = [[x1,x2,x3,x4],x5,x6] and
W3: ex H being strict Ring st
( G = H & x1 = the carrier of H & x2 = the addF of H & x3 = comp H & x4 = 0. H & x5 = the multF of H & x6 = 1. H ) by W2, Def15;
reconsider G = G as strict Element of RingObjects UN by W3;
reconsider ii = ID G as Morphism of (RingCat UN) ;
reconsider ia = ii as RingMorphismStr ;
A: dom ii = dom ia by Def19
.= a ;
cod ii = cod ia by Def20
.= a ;
then ii in Hom (a,a) by A;
hence Hom (a,a) <> {} ; :: thesis:

end;