theorem :: MOD_3:22

for R being Skew-Field
for V being LeftMod of R
for A being Subset of V st Lin A = V holds
ex I being Basis of V st I c= A