set C = RingCat UN;
let a be Element of (RingCat UN); CAT_1:def 10 ex b1 being Morphism of a,a st
for b2 being Element of the carrier of (RingCat UN) holds
( ( Hom (a,b2) = {} or for b3 being Morphism of a,b2 holds b3 (*) b1 = b3 ) & ( Hom (b2,a) = {} or for b3 being Morphism of b2,a holds b1 (*) b3 = b3 ) )
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
; for b1 being Element of the carrier of (RingCat UN) holds
( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) ii = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds ii (*) b2 = b2 ) )
thus
for b1 being Element of the carrier of (RingCat UN) holds
( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) ii = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds ii (*) b2 = b2 ) )
by Lm11; verum