set i = GroupMorphismStr(# G,G,(id G) #);
fun GroupMorphismStr(# G,G,(id G) #) = id G ;
hence GroupMorphismStr(# G,G,(id G) #) is Morphism of G,G by Th10; :: thesis: verum