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

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