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 S1[ set ] means ( \$1 is Subset of X implies ex l being Linear_Combination of singletons X st Sum l = \$1 );
A1: S1[ {} ]
proof
reconsider l = ZeroLC () 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 = 0. () by VECTSP_6:15;
hence Sum l = {} ; :: thesis: verum
end;
A2: for x, B being set st x in A & B c= A & S1[B] holds
S1[B \/ {x}]
proof
let x, B be set ; :: thesis: ( x in A & B c= A & S1[B] implies S1[B \/ {x}] )
assume that
x in A and
B c= A and
A3: S1[B] ; :: thesis: S1[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 ; :: 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 () as Linear_Combination of {} () by VECTSP_6:5;
reconsider f = {x} as Element of () by ;
reconsider g = f as Subset of X ;
set m = z +* (f,());
z +* (f,()) is Linear_Combination of ({} ()) \/ {f} by RANKNULL:23;
then reconsider m = z +* (f,()) as Linear_Combination of {f} ;
dom z = [#] () 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
.= B \+\ g by
.= (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 ;
S1[A] from FINSET_1:sch 2(A9, A1, A2);
hence ex l being Linear_Combination of singletons X st Sum l = A ; :: thesis: verum