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 Th56, A1;
then A = {} ;
hence {} is Basis of RealVectSpace (Seg 0 ) by A1; :: thesis: verum