:: deftheorem defines ID RINGCAT1:def 6 :
for G being Ring holds ID G = RingMorphismStr(# G,G,(id G) #);