let UN be Universe; :: thesis: for b being Object of
for b' being Element of RingObjects UN st b = b' holds
id b = ID b'
set C = RingCat UN;
set V = RingObjects UN;
let b be Object of ; :: thesis: for b' being Element of RingObjects UN st b = b' holds
id b = ID b'
let b' be Element of RingObjects UN; :: thesis: ( b = b' implies id b = ID b' )
assume b = b' ; :: thesis: id b = ID b'
hence id b = (ID (RingObjects UN)) . b' by CAT_1:def 5
.= ID b' by Def22 ;
:: thesis: verum