set i = LModMorphismStr(# G,G,(id G) #);
( dom LModMorphismStr(# G,G,(id G) #) = G & cod LModMorphismStr(# G,G,(id G) #) = G & fun LModMorphismStr(# G,G,(id G) #) = id G ) ;
hence LModMorphismStr(# G,G,(id G) #) is strict Morphism of G,G by Th11, Th13; :: thesis: verum