let V be free Z_Module; :: 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 Z_ModuleStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) ;
hence v in Lin I by Def2; :: thesis: verum