ex AA being finite Subset of (Lin A) st AA is Basis 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 AA = A as finite linearly-independent Subset of (Lin A) by Th16, TARSKI:def 3;
take AA ; :: thesis: AA is Basis of (Lin A)
Lin A = Lin AA by Th20;
hence AA is Basis of (Lin A) by VECTSP_7:def 3; :: thesis: verum
end;
hence Lin A is finite-rank ; :: thesis: verum