for G being Ring holds
( dom (ID G) = G & cod (ID G) = G & ( for f being strict RingMorphism st cod f = G holds
(ID G) * f = f ) & ( for g being strict RingMorphism st dom g = G holds
g * (ID G) = g ) )