let V be LeftMod of INT.Ring ; :: thesis: for A being linearly-independent Subset of V holds A is Basis of (Lin A)
let A be linearly-independent Subset of V; :: thesis: A is Basis of (Lin A)
reconsider AA = A as Subset of (Lin A) by ThLin4;
(Omega). (Lin A) = Lin AA by ZMODUL03:20;
hence A is Basis of (Lin A) by ZMODUL03:16, VECTSP_7:def 3; :: thesis: verum