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

( 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