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: A is finite ;
A2: S₁[ {} ]

proof

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

end;

A4: 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
A5: S₁[B] ; :: thesis: S₁[B \/ {x}]
assume A6: 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
A7: Sum l = B by A5;

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

suppose A8: 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 A7, A8, ZFMISC_1:46; :: thesis: verum

end;

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

reconsider f = {x} as Element of (bspace X) by A6, XBOOLE_1:11;
reconsider g = f as Subset of X ;
reconsider z = ZeroLC (bspace X) as Linear_Combination of {} (bspace X) by VECTSP_6:26;
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:169;
then A10: m . f = 1_ Z_2 by FUNCT_7:33;
A11: B misses {x} by A9, ZFMISC_1:56;
f in singletons X ;
then {f} c= singletons X by ZFMISC_1:37;
then m is Linear_Combination of singletons X by VECTSP_6:25;
then reconsider n = l + m as Linear_Combination of singletons X by VECTSP_6:52;
A12: Sum n = (Sum l) + (Sum m) by VECTSP_6:77
.= (Sum l) + ((m . f) * f) by VECTSP_6:43
.= (Sum l) + f by A10, VECTSP_1:def 26
.= B \+\ g by A7, Def5
.= (B \/ {x}) \ (B /\ {x}) by XBOOLE_1:101
.= (B \/ {x}) \ {} by A11, XBOOLE_0:def 7
.= B \/ {x} ;
take n ; :: thesis: Sum n = B \/ {x}
thus Sum n = B \/ {x} by A12; :: thesis: verum

end;

end;

end;

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