set i = GroupMorphismStr(# G,G,(id G) #);
( dom GroupMorphismStr(# G,G,(id G) #) = G & cod GroupMorphismStr(# G,G,(id G) #) = G & fun GroupMorphismStr(# G,G,(id G) #) = id G ) ;
hence GroupMorphismStr(# G,G,(id G) #) is Morphism of G,G by Th19, Th21; :: thesis: verum