let V be RealLinearSpace; :: 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 RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) by STRUCT_0:def 5;

hence v in Lin I by RLVECT_3:def 3; :: thesis: verum

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 RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) by STRUCT_0:def 5;

hence v in Lin I by RLVECT_3:def 3; :: thesis: verum