theorem :: VECTSP_7:26

for R being domRing
for V being strict LeftMod of R
for A being Subset of V st not R is degenerated & A = the carrier of V holds
Lin A = V