let R be Skew-Field; :: thesis: for V being LeftMod of R holds V is free
let V be LeftMod of R; :: thesis: V is free
ex B being Subset of V st B is base by Lm3;
hence V is free by Def3; :: thesis: verum