let V be RealUnitarySpace; :: thesis: for A being Subset of V st V is finite-dimensional & A is linearly-independent holds

A is finite

let A be Subset of V; :: thesis: ( V is finite-dimensional & A is linearly-independent implies A is finite )

assume that

A1: V is finite-dimensional and

A2: A is linearly-independent ; :: thesis: A is finite

consider B being Basis of V such that

A3: A c= B by A2, RUSUB_3:15;

B is finite by A1, Th3;

hence A is finite by A3; :: thesis: verum

A is finite

let A be Subset of V; :: thesis: ( V is finite-dimensional & A is linearly-independent implies A is finite )

assume that

A1: V is finite-dimensional and

A2: A is linearly-independent ; :: thesis: A is finite

consider B being Basis of V such that

A3: A c= B by A2, RUSUB_3:15;

B is finite by A1, Th3;

hence A is finite by A3; :: thesis: verum