consider A being finite Subset of V such that
A1:
A is Basis of V
by Def1;
consider p being FinSequence such that
A2:
rng p = A
and
A3:
p is one-to-one
by FINSEQ_4:58;
reconsider p = p as FinSequence of V by A2, FINSEQ_1:def 4;
take f = p; ( f is one-to-one & rng f is Basis of V )
thus
f is one-to-one
by A3; rng f is Basis of V
thus
rng f is Basis of V
by A1, A2; verum