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