let UN be Universe; :: thesis: for a being Object of (GroupCat UN)
for aa being Element of GroupObjects UN st a = aa holds
id a = ID aa
let a be Object of (GroupCat UN); :: thesis: for aa being Element of GroupObjects UN st a = aa holds
id a = ID aa
let aa be Element of GroupObjects UN; :: thesis: ( a = aa implies id a = ID aa )
set C = GroupCat UN;
assume A1: a = aa ; :: thesis: id a = ID aa
reconsider ii = ID aa as Morphism of (GroupCat UN) ;
reconsider ia = ii as GroupMorphismStr ;
A2: dom ii = dom ia by Def25
.= a by A1 ;
cod ii = cod ia by Def26
.= a by A1 ;
then reconsider ii = ii as Morphism of a,a by A2, CAT_1:4;
for b being Object of (GroupCat 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, Lm2;
hence id a = ID aa by CAT_1:def 12; :: thesis: verum