set i = RingMorphismStr(# G,G,(id G) #);
( dom RingMorphismStr(# G,G,(id G) #) = G & cod RingMorphismStr(# G,G,(id G) #) = G & fun RingMorphismStr(# G,G,(id G) #) = id G ) ;
hence RingMorphismStr(# G,G,(id G) #) is RingMorphism by Def6; :: thesis: verum