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 b' = b as Element of GroupObjects UN ;
reconsider b'' = b' as AddGroup ;
A1: id b = ID b' by Th48;
hence A2: dom (id b) = dom (ID b'') 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 b'') 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 f' = f1 as strict GroupMorphism ;
A5: cod f' = b'' by A4, Def33;
thus (id b) * f = (ID b'') * f' 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 f' = f1 as strict GroupMorphism ;
A7: dom f' = b'' by A6, Def32;
thus f * (id b) = f' * (ID b'') by A1, A3, A6, Th50
.= f by A7, Th34 ; :: thesis: verum

end;