consider A being finite Subset of (REAL-L 0 ) such that
A1: A is Basis of REAL-L 0 by RLVECT_5:def 1;
card A = 0 by Th56, A1;
then A = {} ;
hence {} is Basis of REAL-L 0 by A1; :: thesis: verum