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 #) )
proof
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;
hence ( (Omega). V is strict & (Omega). V is free ) ; :: thesis: verum