let GF be Field; :: thesis: for V being VectSp of GF
for I being Basis of V
for v being Vector of V holds v in Lin I
let V be VectSp of GF; :: thesis: for I being Basis of V
for v being Vector of V holds v in Lin I
let I be Basis of V; :: thesis: for v being Vector of V holds v in Lin I
let v be Vector of V; :: thesis: v in Lin I
v in VectSpStr(# the carrier of V,the U5 of V,the U2 of V,the lmult of V #) by STRUCT_0:def 5;
hence v in Lin I by VECTSP_7:def 3; :: thesis: verum