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
A1: v in ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) ;
for I being Subset of V holds
( I is base iff ( I is linearly-independent & Lin I = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) ) ) ;
hence v in Lin I by A1; :: thesis: verum