let V be Z_Module; :: thesis: ( (Omega). V is free implies V is free )
assume A1: (Omega). V is free ; :: thesis: V is free
consider I being Subset of ((Omega). V) such that
a2: I is base by VECTSP_7:def 4, A1;
A2: ( I is linearly-independent & (Omega). V = Lin I ) by a2, VECTSP_7:def 3;
reconsider II = I as linearly-independent Subset of V by A2, ZMODUL03:15;
(Omega). V = Lin II by A2, ZMODUL03:20;
then II is base by VECTSP_7:def 3;
hence V is free by VECTSP_7:def 4; :: thesis: verum