let X be finite set ; :: thesis: singletons X is Basis of (bspace X)
( singletons X is linearly-independent & Lin (singletons X) = bspace X ) by Th36, Th39;
hence singletons X is Basis of (bspace X) by VECTSP_7:def 3; :: thesis: verum