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