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

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