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

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