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