for x being Element of LModObjects UN,R holds x is strict LeftMod of strict by Th9;
hence LModObjects UN,R is LeftMod_DOMAIN of R by Def1; :: thesis: verum