let B be Basis of (VecSp (E,F)); :: thesis: B is finite
VecSp (E,F) is finite-dimensional by FIELD_4:def 8;
hence B is finite by VECTSP_9:20; :: thesis: verum