let F be Field; :: thesis: for V being VectSp of F
for A being Subset of V st A is linearly-independent holds
A is Basis of (Lin A)
let V be VectSp of F; :: thesis: for A being Subset of V st A is linearly-independent holds
A is Basis of (Lin A)
let A be Subset of V; :: thesis: ( A is linearly-independent implies A is Basis of (Lin A) )
assume A1: A is linearly-independent ; :: thesis: A is Basis of (Lin A)
A c= [#] (Lin A)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in [#] (Lin A) )
assume A2: x in A ; :: thesis: x in [#] (Lin A)
reconsider x = x as Element of V by A2;
x in Lin A by A2, VECTSP_7:8;
hence x in [#] (Lin A) ; :: thesis: verum

end;

then reconsider B = A as Subset of (Lin A) ;
A3: Lin B = Lin A by VECTSP_9:17;
B is linearly-independent by A1, VECTSP_9:12;
hence A is Basis of (Lin A) by A3, VECTSP_7:def 3; :: thesis: verum