let X be finite set ; :: thesis: for A being Subset of X ex l being Linear_Combination of singletons X st Sum l = A
let A be Subset of X; :: thesis: ex l being Linear_Combination of singletons X st Sum l = A
set V = bspace X;
set S = singletons X;
defpred S₁[ set ] means ( $1 is Subset of X implies ex l being Linear_Combination of singletons X st Sum l = $1 );
A1: S₁[ {} ]

proof

reconsider l = ZeroLC (bspace X) as Linear_Combination of singletons X by VECTSP_6:5;
assume {} is Subset of X ; :: thesis: ex l being Linear_Combination of singletons X st Sum l = {}
take l ; :: thesis: Sum l = {}
Sum l = 0. (bspace X) by VECTSP_6:15;
hence Sum l = {} ; :: thesis: verum

end;

A2: for x, B being set st x in A & B c= A & S₁[B] holds
S₁[B \/ {x}]

proof

let x, B be set ; :: thesis: ( x in A & B c= A & S₁[B] implies S₁[B \/ {x}] )
assume that
x in A and
B c= A and
A3: S₁[B] ; :: thesis: S₁[B \/ {x}]
assume A4: B \/ {x} is Subset of X ; :: thesis: ex l being Linear_Combination of singletons X st Sum l = B \/ {x}
then reconsider B = B as Subset of X by XBOOLE_1:11;
consider l being Linear_Combination of singletons X such that
A5: Sum l = B by A3;

per cases ( x in B or not x in B ) ;

suppose A6: x in B ; :: thesis: ex l being Linear_Combination of singletons X st Sum l = B \/ {x}

take l ; :: thesis: Sum l = B \/ {x}
thus Sum l = B \/ {x} by A5, A6, ZFMISC_1:40; :: thesis: verum

end;

suppose not x in B ; :: thesis: ex l being Linear_Combination of singletons X st Sum l = B \/ {x}

then A7: B misses {x} by ZFMISC_1:50;
reconsider z = ZeroLC (bspace X) as Linear_Combination of {} (bspace X) by VECTSP_6:5;
reconsider f = {x} as Element of (bspace X) by A4, XBOOLE_1:11;
reconsider g = f as Subset of X ;
set m = z +* (f,(1_ Z_2));
z +* (f,(1_ Z_2)) is Linear_Combination of ({} (bspace X)) \/ {f} by RANKNULL:23;
then reconsider m = z +* (f,(1_ Z_2)) as Linear_Combination of {f} ;
dom z = [#] (bspace X) by FUNCT_2:92;
then A8: m . f = 1_ Z_2 by FUNCT_7:31;
f in singletons X ;
then {f} c= singletons X by ZFMISC_1:31;
then m is Linear_Combination of singletons X by VECTSP_6:4;
then reconsider n = l + m as Linear_Combination of singletons X by VECTSP_6:24;
take n ; :: thesis: Sum n = B \/ {x}
Sum n = (Sum l) + (Sum m) by VECTSP_6:44
.= (Sum l) + ((m . f) * f) by VECTSP_6:17
.= (Sum l) + f by A8
.= B \+\ g by A5, Def5
.= (B \/ {x}) \ (B /\ {x}) by XBOOLE_1:101
.= (B \/ {x}) \ {} by A7
.= B \/ {x} ;
hence Sum n = B \/ {x} ; :: thesis: verum

end;

end;

end;

A9: A is finite ;
S₁[A] from FINSET_1:sch 2(A9, A1, A2);
hence ex l being Linear_Combination of singletons X st Sum l = A ; :: thesis: verum