let GF be Field; :: thesis: for V being VectSp of GF st V is finite-dimensional holds
for A being Subset of V st A is linearly-independent holds
A is finite
let V be VectSp of GF; :: thesis: ( V is finite-dimensional implies for A being Subset of V st A is linearly-independent holds
A is finite )
assume A1: V is finite-dimensional ; :: thesis: for A being Subset of V st A is linearly-independent holds
A is finite
let A be Subset of V; :: thesis: ( A is linearly-independent implies A is finite )
assume A is linearly-independent ; :: thesis: A is finite
then consider B being Basis of V such that
A2: A c= B by VECTSP_7:19;
B is finite by A1;
hence A is finite by A2; :: thesis: verum