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