let G be AddGroup; :: thesis: ( dom (ID G) = G & cod (ID G) = G & ( for f being strict GroupMorphism st cod f = G holds
(ID G) * f = f ) & ( for g being strict GroupMorphism st dom g = G holds
g * (ID G) = g ) )
set i = ID G;
thus dom (ID G) = G ; :: thesis: ( cod (ID G) = G & ( for f being strict GroupMorphism st cod f = G holds
(ID G) * f = f ) & ( for g being strict GroupMorphism st dom g = G holds
g * (ID G) = g ) )
thus cod (ID G) = G ; :: thesis: ( ( for f being strict GroupMorphism st cod f = G holds
(ID G) * f = f ) & ( for g being strict GroupMorphism st dom g = G holds
g * (ID G) = g ) )
thus for f being strict GroupMorphism st cod f = G holds
(ID G) * f = f :: thesis: for g being strict GroupMorphism st dom g = G holds
g * (ID G) = g

proof

let f be strict GroupMorphism; :: thesis: ( cod f = G implies (ID G) * f = f )
assume A1: cod f = G ; :: thesis: (ID G) * f = f
set H = dom f;
reconsider f' = f as Morphism of dom f,G by A1, Def19;
A2: dom (ID G) = G ;
consider m being Function of (dom f),G such that
A3: f' = GroupMorphismStr(# (dom f),G,m #) by Th23;
(id G) * m = m by FUNCT_2:23;
hence (ID G) * f = f by A1, A2, A3, Def21; :: thesis: verum

end;

thus for g being strict GroupMorphism st dom g = G holds
g * (ID G) = g :: thesis: verum

proof

let f be strict GroupMorphism; :: thesis: ( dom f = G implies f * (ID G) = f )
assume A4: dom f = G ; :: thesis: f * (ID G) = f
set H = cod f;
reconsider f' = f as Morphism of G, cod f by A4, Def19;
A5: cod (ID G) = G ;
consider m being Function of G,(cod f) such that
A6: f' = GroupMorphismStr(# G,(cod f),m #) by Th23;
m * (id G) = m by FUNCT_2:23;
hence f * (ID G) = f by A4, A5, A6, Def21; :: thesis: verum

end;