let V be RealLinearSpace; :: thesis:
let Af be finite Subset of V; :: thesis:
let If be finite affinely-independent Subset of V; :: thesis:
defpred S₁[ Nat] means for B being finite Subset of V st card B = $1 & B c= conv If holds
for L being Linear_Combination of B st Carrier L = B & sum L = 1 holds
( Sum L in Affin If & ( for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st
( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds
F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) ) );
A1: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis:
assume A2: S₁[m] ; :: thesis:
let B be finite Subset of V; :: thesis:
assume that
A3: card B = m + 1 and
A4: B c= conv If ; :: thesis:
conv If c= Affin If by RLAFFIN1:65;
then A5: B c= Affin If by A4;
then A6: Affin B c= Affin If by RLAFFIN1:51;
let L be Linear_Combination of B; :: thesis:
assume that
A7: Carrier L = B and
A8: sum L = 1 ; :: thesis:
Sum L in { (Sum K) where K is Linear_Combination of B : sum K = 1 } by A8;
then Sum L in Affin B by RLAFFIN1:59;
hence Sum L in Affin If by A6; :: thesis:

per cases ;

suppose A9: m = 0 ; :: thesis:

let x be Element of V; :: thesis:
consider b being object such that
A10: B = {b} by A3, A9, CARD_2:42;
b in B by A10, TARSKI:def 1;
then reconsider b = b as Element of V ;
A11: sum L = L . b by A7, A10, RLAFFIN1:32;
set F = <*((b |-- If) . x)*>;
set G = <*b*>;
take <*((b |-- If) . x)*> ; :: thesis:
take <*b*> ; :: thesis:
Sum L = (L . b) * b by A10, RLVECT_2:32;
then ( len <*b*> = 1 & Sum L = b ) by A8, A11, FINSEQ_1:39, RLVECT_1:def 8;
hence ( ((Sum L) |-- If) . x = Sum <*((b |-- If) . x)*> & len <*b*> = len <*((b |-- If) . x)*> & <*b*> is one-to-one & rng <*b*> = Carrier L ) by A7, A10, FINSEQ_1:39, FINSEQ_3:93, RVSUM_1:73; :: thesis:
let n be Nat; :: thesis:
assume n in dom <*((b |-- If) . x)*> ; :: thesis:
then n in Seg 1 by FINSEQ_1:38;
then A12: n = 1 by FINSEQ_1:2, TARSKI:def 1;
then <*b*> . n = b by FINSEQ_1:40;
hence <*((b |-- If) . x)*> . n = (L . (<*b*> . n)) * (((<*b*> . n) |-- If) . x) by A8, A11, A12, FINSEQ_1:40; :: thesis:

end;

suppose A13: m > 0 ; :: thesis:

ex v being Element of V st
( L . v <> 1 & v in Carrier L )

proof

consider F being FinSequence of V such that
A14: F is one-to-one and
A15: rng F = Carrier L and
A16: 1 = Sum (L * F) by A8, RLAFFIN1:def 3;
dom F,B are_equipotent by A7, A14, A15, WELLORD2:def 4;
then A17: card B = card (dom F) by CARD_1:5
.= card (Seg (len F)) by FINSEQ_1:def 3
.= len F by FINSEQ_1:57 ;
A18: ( len F = len (L * F) & len ((len F) |-> 1) = len F ) by CARD_1:def 7, FINSEQ_2:33;
Sum ((len F) |-> 1) = (len F) * 1 by RVSUM_1:80;
then (len F) |-> 1 <> L * F by A3, A13, A16, A17;
then consider k being Nat such that
A19: ( 1 <= k & k <= len F ) and
A20: ((len F) |-> 1) . k <> (L * F) . k by A18, FINSEQ_1:14;
A21: k in Seg (len F) by A19, FINSEQ_1:1;
A22: k in dom F by A19, FINSEQ_3:25;
then A23: F . k in Carrier L by A15, FUNCT_1:def 3;
L . (F . k) = (L * F) . k by A22, FUNCT_1:13;
then L . (F . k) <> 1 by A20, A21, FINSEQ_2:57;
hence ex v being Element of V st
( L . v <> 1 & v in Carrier L ) by A23; :: thesis:

end;

then consider v being Element of V such that
A24: L . v <> 1 and
A25: v in Carrier L ;
set 1Lv = 1 - (L . v);
consider K being Linear_Combination of {v} such that
A26: K . v = L . v by RLVECT_4:37;
set LK = L - K;
A27: 1 - (L . v) <> 0 by A24;
set 1LK = (1 / (1 - (L . v))) * (L - K);
A28: Carrier K c= {v} by RLVECT_2:def 6;
then sum K = K . v by RLAFFIN1:32;
then sum (L - K) = 1 - (L . v) by A8, A26, RLAFFIN1:36;
then A29: sum ((1 / (1 - (L . v))) * (L - K)) = (1 / (1 - (L . v))) * (1 - (L . v)) by RLAFFIN1:35;
(L - K) . v = (L . v) - (K . v) by RLVECT_2:54;
then A30: not v in Carrier (L - K) by A26, RLVECT_2:19;
A31: card (B \ {v}) = m by A3, A7, A25, STIRL2_1:55;
A32: Sum K = (L . v) * v by A26, RLVECT_2:32;
B \ {v} c= B by XBOOLE_1:36;
then A33: B \ {v} c= conv If by A4;
L . v <> 0 by A25, RLVECT_2:19;
then v in Carrier K by A26;
then A34: Carrier K = {v} by A28, ZFMISC_1:33;
A35: B \ {v} c= Carrier (L - K)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A36: x in B \ {v} ; :: thesis:
then reconsider u = x as Element of V ;
u in B by A36, ZFMISC_1:56;
then A37: L . u <> 0 by A7, RLVECT_2:19;
( (L - K) . u = (L . u) - (K . u) & not u in {v} ) by A36, RLVECT_2:54, XBOOLE_0:def 5;
then (L - K) . u <> 0 by A34, A37;
hence x in Carrier (L - K) ; :: thesis:

end;

let x be Element of V; :: thesis:
A38: (1 / (1 - (L . v))) * (1 - (L . v)) = (1 * (1 - (L . v))) / (1 - (L . v)) by XCMPLX_1:74
.= 1 by A27, XCMPLX_1:60 ;
Sum ((1 / (1 - (L . v))) * (L - K)) = (1 / (1 - (L . v))) * (Sum (L - K)) by RLVECT_3:2;
then (1 - (L . v)) * (Sum ((1 / (1 - (L . v))) * (L - K))) = ((1 - (L . v)) * (1 / (1 - (L . v)))) * (Sum (L - K)) by RLVECT_1:def 7
.= Sum (L - K) by A38, RLVECT_1:def 8 ;
then A39: ((1 - (L . v)) * (Sum ((1 / (1 - (L . v))) * (L - K)))) + ((L . v) * v) = ((Sum L) - ((L . v) * v)) + ((L . v) * v) by A32, RLVECT_3:4
.= Sum L by RLVECT_4:1 ;
B \/ {v} = B by A7, A25, ZFMISC_1:40;
then Carrier (L - K) c= B \ {v} by A7, A34, A30, RLVECT_2:55, ZFMISC_1:34;
then B \ {v} = Carrier (L - K) by A35;
then A40: Carrier ((1 / (1 - (L . v))) * (L - K)) = B \ {v} by A27, RLVECT_2:42;
then A41: (1 / (1 - (L . v))) * (L - K) is Linear_Combination of B \ {v} by RLVECT_2:def 6;
then consider F being FinSequence of REAL , G being FinSequence of V such that
A42: ((Sum ((1 / (1 - (L . v))) * (L - K))) |-- If) . x = Sum F and
A43: len G = len F and
A44: G is one-to-one and
A45: rng G = Carrier ((1 / (1 - (L . v))) * (L - K)) and
A46: for n being Nat st n in dom F holds
F . n = (((1 / (1 - (L . v))) * (L - K)) . (G . n)) * (((G . n) |-- If) . x) by A2, A29, A38, A31, A33, A40;
Sum ((1 / (1 - (L . v))) * (L - K)) in Affin If by A2, A29, A38, A31, A33, A40, A41;
then A47: (Sum L) |-- If = ((1 - (L . v)) * ((Sum ((1 / (1 - (L . v))) * (L - K))) |-- If)) + ((L . v) * (v |-- If)) by A5, A7, A25, A39, RLAFFIN1:70;
take F1 = ((1 - (L . v)) * F) ^ <*((L . v) * ((v |-- If) . x))*>; :: thesis:
take G1 = G ^ <*v*>; :: thesis:
thus Sum F1 = (Sum ((1 - (L . v)) * F)) + ((L . v) * ((v |-- If) . x)) by RVSUM_1:74
.= ((1 - (L . v)) * (((Sum ((1 / (1 - (L . v))) * (L - K))) |-- If) . x)) + ((L . v) * ((v |-- If) . x)) by A42, RVSUM_1:87
.= (((1 - (L . v)) * ((Sum ((1 / (1 - (L . v))) * (L - K))) |-- If)) . x) + ((L . v) * ((v |-- If) . x)) by RLVECT_2:def 11
.= (((1 - (L . v)) * ((Sum ((1 / (1 - (L . v))) * (L - K))) |-- If)) . x) + (((L . v) * (v |-- If)) . x) by RLVECT_2:def 11
.= ((Sum L) |-- If) . x by A47, RLVECT_2:def 10 ; :: thesis:
reconsider f = F as Element of (len F) -tuples_on REAL by FINSEQ_2:92;
A48: len F = len ((1 - (L . v)) * f) by CARD_1:def 7;
then A49: len F1 = (len F) + 1 by FINSEQ_2:16;
hence len F1 = len G1 by A43, FINSEQ_2:16; :: thesis:
A50: rng <*v*> = {v} by FINSEQ_1:38;
then ( <*v*> is one-to-one & rng G misses rng <*v*> ) by A40, A45, FINSEQ_3:93, XBOOLE_1:79;
hence G1 is one-to-one by A44, FINSEQ_3:91; :: thesis:
thus rng G1 = (B \ {v}) \/ {v} by A40, A45, A50, FINSEQ_1:31
.= Carrier L by A7, A25, ZFMISC_1:116 ; :: thesis:
let n be Nat; :: thesis:
assume A51: n in dom F1 ; :: thesis:
then A52: n <= len F1 by FINSEQ_3:25;

per cases by A49, A51, A52, FINSEQ_3:25, NAT_1:8;

suppose A53: ( 1 <= n & n <= len F ) ; :: thesis:

then n in dom F by FINSEQ_3:25;
then A54: ( ((1 - (L . v)) * f) . n = (1 - (L . v)) * (f . n) & F . n = (((1 / (1 - (L . v))) * (L - K)) . (G . n)) * (((G . n) |-- If) . x) ) by A46, RVSUM_1:45;
A55: n in dom G by A43, A53, FINSEQ_3:25;
then A56: G1 . n = G . n by FINSEQ_1:def 7;
A57: G . n in B \ {v} by A40, A45, A55, FUNCT_1:def 3;
then not G . n in {v} by XBOOLE_0:def 5;
then K . (G . n) = 0 by A34, A57;
then (L - K) . (G . n) = (L . (G . n)) - 0 by A57, RLVECT_2:54;
then ((1 / (1 - (L . v))) * (L - K)) . (G . n) = (1 / (1 - (L . v))) * (L . (G . n)) by A57, RLVECT_2:def 11;
then (1 - (L . v)) * (((1 / (1 - (L . v))) * (L - K)) . (G1 . n)) = ((1 - (L . v)) * (1 / (1 - (L . v)))) * (L . (G . n)) by A56;
then A58: (1 - (L . v)) * (((1 / (1 - (L . v))) * (L - K)) . (G1 . n)) = L . (G . n) by A38;
n in dom ((1 - (L . v)) * F) by A48, A53, FINSEQ_3:25;
hence F1 . n = (L . (G1 . n)) * (((G1 . n) |-- If) . x) by A54, A56, A58, FINSEQ_1:def 7; :: thesis:

end;

suppose A59: n = (len F) + 1 ; :: thesis:

then G1 . n = v by A43, FINSEQ_1:42;
hence F1 . n = (L . (G1 . n)) * (((G1 . n) |-- If) . x) by A48, A59, FINSEQ_1:42; :: thesis:

end;

let L be Linear_Combination of Af; :: thesis:
assume that
A60: Af c= conv If and
A61: sum L = 1 ; :: thesis:
set C = Carrier L;
Carrier L c= Af by RLVECT_2:def 6;
then A62: Carrier L c= conv If by A60;
reconsider L1 = L as Linear_Combination of Carrier L by RLVECT_2:def 6;
A63: S₁[ 0 ]

proof

let B be finite Subset of V; :: thesis:
assume that
A64: card B = 0 and
B c= conv If ; :: thesis:
let L be Linear_Combination of B; :: thesis:
assume that
Carrier L = B and
A65: sum L = 1 ; :: thesis:
B = {} the carrier of V by A64;
then L = ZeroLC V by RLVECT_2:23;
hence ( Sum L in Affin If & ( for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st
( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds
F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) ) ) by A65, RLAFFIN1:31; :: thesis:

end;

for m being Nat holds S₁[m] from NAT_1:sch 2(A63, A1);
then ( sum L = sum L1 & S₁[ card (Carrier L)] ) ;
hence ( Sum L in Affin If & ( for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st
( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds
F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) ) ) by A61, A62; :: thesis: