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

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