set C = RingCat UN;
let a be Element of (RingCat UN); :: according to CAT_1:def 10 :: thesis: ex b₁ being Morphism of a,a st
for b₂ being Element of the carrier of (RingCat UN) holds
( ( Hom (a,b₂) = {} or for b₃ being Morphism of a,b₂ holds b₃ (*) b₁ = b₃ ) & ( Hom (b₂,a) = {} or for b₃ being Morphism of b₂,a holds b₁ (*) b₃ = b₃ ) )
reconsider aa = a as Element of RingObjects UN ;
reconsider ii = ID aa as Morphism of (RingCat UN) ;
reconsider ia = ii as RingMorphismStr ;
A1: dom ii = dom ia by Def19
.= a ;
cod ii = cod ia by Def20
.= a ;
then reconsider ii = ii as Morphism of a,a by A1, CAT_1:4;
take ii ; :: thesis: for b₁ being Element of the carrier of (RingCat UN) holds
( ( Hom (a,b₁) = {} or for b₂ being Morphism of a,b₁ holds b₂ (*) ii = b₂ ) & ( Hom (b₁,a) = {} or for b₂ being Morphism of b₁,a holds ii (*) b₂ = b₂ ) )
thus for b₁ being Element of the carrier of (RingCat UN) holds
( ( Hom (a,b₁) = {} or for b₂ being Morphism of a,b₁ holds b₂ (*) ii = b₂ ) & ( Hom (b₁,a) = {} or for b₂ being Morphism of b₁,a holds ii (*) b₂ = b₂ ) ) by Lm11; :: thesis: verum