ex AA being finite Subset of (Lin A) st AA is Basis of (Lin A)

proof

hence
Lin A is finite-rank
; :: thesis: verum
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;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