reconsider VV = (Omega). V as Z_Module ;
consider A being Subset of V such that
A1: ( A is linearly-independent & Lin A = Z_ModuleStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) ) by Def1;
ex AA being Subset of VV st
( AA is linearly-independent & Lin AA = Z_ModuleStruct(# the carrier of VV, the ZeroF of VV, the addF of VV, the Mult of VV #) )

proof

consider AA being Subset of VV such that
A2: AA = A ;
take AA ; :: thesis: ( AA is linearly-independent & Lin AA = Z_ModuleStruct(# the carrier of VV, the ZeroF of VV, the addF of VV, the Mult of VV #) )
thus ( AA is linearly-independent & Lin AA = Z_ModuleStruct(# the carrier of VV, the ZeroF of VV, the addF of VV, the Mult of VV #) ) by A1, A2, Th16, Th20; :: thesis: verum

end;

hence ( (Omega). V is strict & (Omega). V is free ) ; :: thesis: verum