consider A being finite Subset of V such that

A1: A is Basis of V by ZMODUL03:def 3;

reconsider A = A as Basis of V by A1;

take A ; :: thesis: A is finite

thus A is finite ; :: thesis: verum

A1: A is Basis of V by ZMODUL03:def 3;

reconsider A = A as Basis of V by A1;

take A ; :: thesis: A is finite

thus A is finite ; :: thesis: verum