set i = LModMorphismStr(# G,G,(id G) #);
fun LModMorphismStr(# G,G,(id G) #) = id G ;
hence LModMorphismStr(# G,G,(id G) #) is strict Morphism of G,G by Th5; :: thesis: verum