let F be Field; :: thesis: for V being VectSp of F
for A being Subset of (LinearlyIndependentSubsets V) holds
( A is independent iff A is linearly-independent Subset of V )
let V be VectSp of F; :: thesis: for A being Subset of (LinearlyIndependentSubsets V) holds
( A is independent iff A is linearly-independent Subset of V )
set M = LinearlyIndependentSubsets V;
let B be Subset of (LinearlyIndependentSubsets V); :: thesis: ( B is independent iff B is linearly-independent Subset of V )
the_family_of (LinearlyIndependentSubsets V) = { A where A is Subset of V : A is linearly-independent } by Def8;
then ( B in the_family_of (LinearlyIndependentSubsets V) iff ex A being Subset of V st
( B = A & A is linearly-independent ) ) ;
hence ( B is independent iff B is linearly-independent Subset of V ) ; :: thesis: verum