theorem :: GRCAT_1:23

for G being AddGroup holds
( 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 ) )