let V be free finite-rank Z_Module; :: thesis: rank V = rank ((Omega). V)

consider I being finite Subset of V such that

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

A2: (Omega). V = Lin I by A1, VECTSP_7:def 3;

( card I = rank V & I is linearly-independent ) by A1, ZMODUL03:def 5, VECTSP_7:def 3;

hence rank V = rank ((Omega). V) by A2, RL5Th30; :: thesis: verum

consider I being finite Subset of V such that

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

A2: (Omega). V = Lin I by A1, VECTSP_7:def 3;

( card I = rank V & I is linearly-independent ) by A1, ZMODUL03:def 5, VECTSP_7:def 3;

hence rank V = rank ((Omega). V) by A2, RL5Th30; :: thesis: verum