let X be finite set ; :: thesis: Lin (singletons X) = bspace X
set V = bspace X;
set S = singletons X;
for v being Element of (bspace X) holds v in Lin (singletons X)

proof

let v be Element of (bspace X); :: thesis: v in Lin (singletons X)
reconsider f = v as Subset of X ;
consider A being set such that
A1: A c= X and
A2: f = A ;
reconsider A = A as Subset of X by A1;
ex l being Linear_Combination of singletons X st Sum l = A by Th38;
hence v in Lin (singletons X) by A2, VECTSP_7:7; :: thesis: verum

end;

hence Lin (singletons X) = bspace X by VECTSP_4:32; :: thesis: verum