ex B being Subset of (Lin A) st B is base

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 base
Lin B = ModuleStr(# the carrier of (Lin A), the addF of (Lin A), the ZeroF of (Lin A), the lmult of (Lin A) #) by Th20;
hence B is base ; :: thesis: verum

end;

hence Lin A is free ; :: thesis: verum