let V be RealLinearSpace; :: 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 Th2;

B is finite by A1, Th23;

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

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 Th2;

B is finite by A1, Th23;

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