let G be Field; :: thesis: for V being VectSp of G
for A being Subset of V st A is linearly-independent holds
A is Basis of (Lin A)
let V be VectSp of G; :: 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)
set W = Lin A;
for x being object st x in A holds
x in the carrier of (Lin A) by STRUCT_0:def 5, VECTSP_7:8;
then reconsider B = A as linearly-independent Subset of (Lin A) by A1, VECTSP_9:12, TARSKI:def 3;
Lin A = Lin B by VECTSP_9:17;
hence A is Basis of (Lin A) by VECTSP_7:def 3; :: thesis: verum