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