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