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