reconsider VV = (Omega). V as Z_Module ;

consider A being Subset of V such that

a1: A is base by VECTSP_7:def 4;

A1: ( A is linearly-independent & Lin A = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) ) by a1;

ex AA being Subset of VV st

( AA is linearly-independent & Lin AA = ModuleStr(# the carrier of VV, the addF of VV, the ZeroF of VV, the lmult of VV #) )

consider A being Subset of V such that

a1: A is base by VECTSP_7:def 4;

A1: ( A is linearly-independent & Lin A = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) ) by a1;

ex AA being Subset of VV st

( AA is linearly-independent & Lin AA = ModuleStr(# the carrier of VV, the addF of VV, the ZeroF of VV, the lmult of VV #) )

proof

hence
( (Omega). V is strict & (Omega). V is free )
; :: thesis: verum
consider AA being Subset of VV such that

A2: AA = A ;

take AA ; :: thesis: ( AA is linearly-independent & Lin AA = ModuleStr(# the carrier of VV, the addF of VV, the ZeroF of VV, the lmult of VV #) )

thus ( AA is linearly-independent & Lin AA = ModuleStr(# the carrier of VV, the addF of VV, the ZeroF of VV, the lmult of VV #) ) by A1, A2, Th16, Th20; :: thesis: verum

end;A2: AA = A ;

take AA ; :: thesis: ( AA is linearly-independent & Lin AA = ModuleStr(# the carrier of VV, the addF of VV, the ZeroF of VV, the lmult of VV #) )

thus ( AA is linearly-independent & Lin AA = ModuleStr(# the carrier of VV, the addF of VV, the ZeroF of VV, the lmult of VV #) ) by A1, A2, Th16, Th20; :: thesis: verum