set i = RingMorphismStr(# G,G,(id G) #);
fun RingMorphismStr(# G,G,(id G) #) = id G ;
hence RingMorphismStr(# G,G,(id G) #) is RingMorphism by Def5; :: thesis: verum