ex B being Subset of (Lin A) st
( B is linearly-independent & Lin B = Z_ModuleStruct(# the carrier of (Lin A), the ZeroF of (Lin A), the addF of (Lin A), the Mult of (Lin A) #) )

proof

for x being object st x in A holds
x in the carrier of (Lin A) by STRUCT_0:def 5, ZMODUL02:65;
then reconsider B = A as linearly-independent Subset of (Lin A) by Th16, TARSKI:def 3;
take B ; :: thesis: ( B is linearly-independent & Lin B = Z_ModuleStruct(# the carrier of (Lin A), the ZeroF of (Lin A), the addF of (Lin A), the Mult of (Lin A) #) )
thus ( B is linearly-independent & Lin B = Z_ModuleStruct(# the carrier of (Lin A), the ZeroF of (Lin A), the addF of (Lin A), the Mult of (Lin A) #) ) by Th20; :: thesis: verum

end;

hence Lin A is free ; :: thesis: verum