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_{1}[ set ] means ( $1 is Subset of X implies ex l being Linear_Combination of singletons X st Sum l = $1 );

A1: S_{1}[ {} ]
_{1}[B] holds

S_{1}[B \/ {x}]

S_{1}[A]
from FINSET_1:sch 2(A9, A1, A2);

hence ex l being Linear_Combination of singletons X st Sum l = A ; :: thesis: verum

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

A1: S

proof

A2:
for x, B being set st x in A & B c= A & S
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;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

S

proof

A9:
A is finite
;
let x, B be set ; :: thesis: ( x in A & B c= A & S_{1}[B] implies S_{1}[B \/ {x}] )

assume that

x in A and

B c= A and

A3: S_{1}[B]
; :: thesis: S_{1}[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;

end;assume that

x in A and

B c= A and

A3: S

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 )
;

end;

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

end;

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, VECTSP_1:def 17

.= 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;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, VECTSP_1:def 17

.= 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

S

hence ex l being Linear_Combination of singletons X st Sum l = A ; :: thesis: verum