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)

set V = bspace X;

set S = singletons X;

for v being Element of (bspace X) holds v in Lin (singletons X)

proof

hence
Lin (singletons X) = bspace X
by VECTSP_4:32; :: thesis: verum
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;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