consider A being finite Subset of V such that
A1: A is Basis of V by MATRLIN:def 1;
reconsider A = A as Basis of V by A1;
take A ; :: thesis: A is finite
thus A is finite ; :: thesis: verum