let UN be Universe; :: thesis: for a being Object of (RingCat UN)
for aa being Element of RingObjects UN st a = aa holds
id a = ID aa
let a be Object of (RingCat UN); :: thesis: for aa being Element of RingObjects UN st a = aa holds
id a = ID aa
let aa be Element of RingObjects UN; :: thesis: ( a = aa implies id a = ID aa )
set C = RingCat UN;
assume A1: a = aa ; :: thesis: id a = ID aa
reconsider ii = ID aa as Morphism of (RingCat UN) ;
reconsider ia = ii as RingMorphismStr ;
A2: dom ii = dom ia by Def19
.= a by A1 ;
cod ii = cod ia by Def20
.= a by A1 ;
then reconsider ii = ii as Morphism of a,a by A2, CAT_1:4;
for b being Object of (RingCat UN) holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) ii = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f ) ) by A1, Lm11;
hence id a = ID aa by CAT_1:def 12; :: thesis: verum