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; :: thesis: ( f is one-to-one & rng f is Basis of V )

thus f is one-to-one by A3; :: thesis: rng f is Basis of V

thus rng f is Basis of V by A1, A2; :: thesis: verum

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; :: thesis: ( f is one-to-one & rng f is Basis of V )

thus f is one-to-one by A3; :: thesis: rng f is Basis of V

thus rng f is Basis of V by A1, A2; :: thesis: verum