let UN be Universe; :: thesis: for b being Object of (GroupCat UN)
for b9 being Element of GroupObjects UN st b = b9 holds
id b = ID b9
set C = GroupCat UN;
set V = GroupObjects UN;
let b be Object of (GroupCat UN); :: thesis: for b9 being Element of GroupObjects UN st b = b9 holds
id b = ID b9
let b9 be Element of GroupObjects UN; :: thesis: ( b = b9 implies id b = ID b9 )
assume b = b9 ; :: thesis: id b = ID b9
hence id b = (ID (GroupObjects UN)) . b9 by CAT_1:def 2
.= ID b9 by Def34 ;
:: thesis: verum