let V be free finite-rank Z_Module; :: 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 )

consider I being finite Subset of V such that

A1: I is Basis of V by ZMODUL03:def 3;

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

then card A c= card I by A1, XXTh3, XBOOLE_0:def 8;

hence A is finite ; :: thesis: verum

A is finite

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

consider I being finite Subset of V such that

A1: I is Basis of V by ZMODUL03:def 3;

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

then card A c= card I by A1, XXTh3, XBOOLE_0:def 8;

hence A is finite ; :: thesis: verum