let UN be Universe; :: thesis: for b being Object of (GroupCat UN) holds
( dom (id b) = b & cod (id b) = b & ( for f being Morphism of (GroupCat UN) st cod f = b holds
(id b) * f = f ) & ( for g being Morphism of (GroupCat UN) st dom g = b holds
g * (id b) = g ) )
set C = GroupCat UN;
set V = GroupObjects UN;
set X = Morphs (GroupObjects UN);
let b be Object of (GroupCat UN); :: thesis: ( dom (id b) = b & cod (id b) = b & ( for f being Morphism of (GroupCat UN) st cod f = b holds
(id b) * f = f ) & ( for g being Morphism of (GroupCat UN) st dom g = b holds
g * (id b) = g ) )
reconsider b9 = b as Element of GroupObjects UN ;
reconsider b99 = b9 as AddGroup ;
A1: id b = ID b9 by Th48;
hence A2: dom (id b) = dom (ID b99) by Def32
.= b ;
:: thesis: ( cod (id b) = b & ( for f being Morphism of (GroupCat UN) st cod f = b holds
(id b) * f = f ) & ( for g being Morphism of (GroupCat UN) st dom g = b holds
g * (id b) = g ) )
thus A3: cod (id b) = cod (ID b99) by A1, Def33
.= b ; :: thesis: ( ( for f being Morphism of (GroupCat UN) st cod f = b holds
(id b) * f = f ) & ( for g being Morphism of (GroupCat UN) st dom g = b holds
g * (id b) = g ) )
thus for f being Morphism of (GroupCat UN) st cod f = b holds
(id b) * f = f :: thesis: for g being Morphism of (GroupCat UN) st dom g = b holds
g * (id b) = g

proof

let f be Morphism of (GroupCat UN); :: thesis: ( cod f = b implies (id b) * f = f )
assume A4: cod f = b ; :: thesis: (id b) * f = f
reconsider f1 = f as strict Element of Morphs (GroupObjects UN) by Th47;
reconsider f9 = f1 as strict GroupMorphism ;
A5: cod f9 = b99 by A4, Def33;
thus (id b) * f = (ID b99) * f9 by A1, A2, A4, Th50
.= f by A5, Th34 ; :: thesis: verum

end;

thus for g being Morphism of (GroupCat UN) st dom g = b holds
g * (id b) = g :: thesis: verum

proof

let f be Morphism of (GroupCat UN); :: thesis: ( dom f = b implies f * (id b) = f )
assume A6: dom f = b ; :: thesis: f * (id b) = f
reconsider f1 = f as strict Element of Morphs (GroupObjects UN) by Th47;
reconsider f9 = f1 as strict GroupMorphism ;
A7: dom f9 = b99 by A6, Def32;
thus f * (id b) = f9 * (ID b99) by A1, A3, A6, Th50
.= f by A7, Th34 ; :: thesis: verum

end;