let V be RealLinearSpace; :: thesis: for Af being finite Subset of V

for If being finite affinely-independent Subset of V

for L being Linear_Combination of Af st Af c= conv If & 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) ) ) ) )

let Af be finite Subset of V; :: thesis: for If being finite affinely-independent Subset of V

for L being Linear_Combination of Af st Af c= conv If & 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) ) ) ) )

let If be finite affinely-independent Subset of V; :: thesis: for L being Linear_Combination of Af st Af c= conv If & 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) ) ) ) )

defpred S_{1}[ 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_{1}[m] holds

S_{1}[m + 1]

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

assume that

A60: Af c= conv If and

A61: sum L = 1 ; :: thesis: ( 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) ) ) ) )

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_{1}[ 0 ]
_{1}[m]
from NAT_1:sch 2(A63, A1);

then ( sum L = sum L1 & S_{1}[ 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: verum

for If being finite affinely-independent Subset of V

for L being Linear_Combination of Af st Af c= conv If & 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) ) ) ) )

let Af be finite Subset of V; :: thesis: for If being finite affinely-independent Subset of V

for L being Linear_Combination of Af st Af c= conv If & 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) ) ) ) )

let If be finite affinely-independent Subset of V; :: thesis: for L being Linear_Combination of Af st Af c= conv If & 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) ) ) ) )

defpred S

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

S

proof

let L be Linear_Combination of Af; :: thesis: ( Af c= conv If & sum L = 1 implies ( Sum L in Affin If & ( for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st
let m be Nat; :: thesis: ( S_{1}[m] implies S_{1}[m + 1] )

assume A2: S_{1}[m]
; :: thesis: S_{1}[m + 1]

let B be finite Subset of V; :: thesis: ( card B = m + 1 & B c= conv If implies 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) ) ) ) ) )

assume that

A3: card B = m + 1 and

A4: B c= conv If ; :: thesis: 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) ) ) ) )

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: ( Carrier L = B & sum L = 1 implies ( 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) ) ) ) ) )

assume that

A7: Carrier L = B and

A8: sum L = 1 ; :: thesis: ( 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) ) ) ) )

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

end;assume A2: S

let B be finite Subset of V; :: thesis: ( card B = m + 1 & B c= conv If implies 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) ) ) ) ) )

assume that

A3: card B = m + 1 and

A4: B c= conv If ; :: thesis: 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) ) ) ) )

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: ( Carrier L = B & sum L = 1 implies ( 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) ) ) ) ) )

assume that

A7: Carrier L = B and

A8: sum L = 1 ; :: thesis: ( 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) ) ) ) )

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

per cases
( m = 0 or m > 0 )
;

end;

suppose A9:
m = 0
; :: thesis: 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) ) )

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

let x be Element of V; :: thesis: 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) ) )

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: ex G being FinSequence of V st

( ((Sum L) |-- If) . x = Sum <*((b |-- If) . x)*> & len G = len <*((b |-- If) . x)*> & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom <*((b |-- If) . x)*> holds

<*((b |-- If) . x)*> . n = (L . (G . n)) * (((G . n) |-- If) . x) ) )

take <*b*> ; :: thesis: ( ((Sum L) |-- If) . x = Sum <*((b |-- If) . x)*> & len <*b*> = len <*((b |-- If) . x)*> & <*b*> is one-to-one & rng <*b*> = Carrier L & ( for n being Nat st n in dom <*((b |-- If) . x)*> holds

<*((b |-- If) . x)*> . n = (L . (<*b*> . n)) * (((<*b*> . n) |-- If) . x) ) )

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: for n being Nat st n in dom <*((b |-- If) . x)*> holds

<*((b |-- If) . x)*> . n = (L . (<*b*> . n)) * (((<*b*> . n) |-- If) . x)

let n be Nat; :: thesis: ( n in dom <*((b |-- If) . x)*> implies <*((b |-- If) . x)*> . n = (L . (<*b*> . n)) * (((<*b*> . n) |-- If) . x) )

assume n in dom <*((b |-- If) . x)*> ; :: thesis: <*((b |-- If) . x)*> . n = (L . (<*b*> . n)) * (((<*b*> . n) |-- If) . x)

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: verum

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

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: ex G being FinSequence of V st

( ((Sum L) |-- If) . x = Sum <*((b |-- If) . x)*> & len G = len <*((b |-- If) . x)*> & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom <*((b |-- If) . x)*> holds

<*((b |-- If) . x)*> . n = (L . (G . n)) * (((G . n) |-- If) . x) ) )

take <*b*> ; :: thesis: ( ((Sum L) |-- If) . x = Sum <*((b |-- If) . x)*> & len <*b*> = len <*((b |-- If) . x)*> & <*b*> is one-to-one & rng <*b*> = Carrier L & ( for n being Nat st n in dom <*((b |-- If) . x)*> holds

<*((b |-- If) . x)*> . n = (L . (<*b*> . n)) * (((<*b*> . n) |-- If) . x) ) )

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: for n being Nat st n in dom <*((b |-- If) . x)*> holds

<*((b |-- If) . x)*> . n = (L . (<*b*> . n)) * (((<*b*> . n) |-- If) . x)

let n be Nat; :: thesis: ( n in dom <*((b |-- If) . x)*> implies <*((b |-- If) . x)*> . n = (L . (<*b*> . n)) * (((<*b*> . n) |-- If) . x) )

assume n in dom <*((b |-- If) . x)*> ; :: thesis: <*((b |-- If) . x)*> . n = (L . (<*b*> . n)) * (((<*b*> . n) |-- If) . x)

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: verum

suppose A13:
m > 0
; :: thesis: 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) ) )

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

ex v being Element of V st

( L . v <> 1 & v in Carrier L )

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)

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

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: ex G being FinSequence of V st

( ((Sum L) |-- If) . x = Sum F1 & len G = len F1 & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F1 holds

F1 . n = (L . (G . n)) * (((G . n) |-- If) . x) ) )

take G1 = G ^ <*v*>; :: thesis: ( ((Sum L) |-- If) . x = Sum F1 & len G1 = len F1 & G1 is one-to-one & rng G1 = Carrier L & ( for n being Nat st n in dom F1 holds

F1 . n = (L . (G1 . n)) * (((G1 . n) |-- If) . x) ) )

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: ( len G1 = len F1 & G1 is one-to-one & rng G1 = Carrier L & ( for n being Nat st n in dom F1 holds

F1 . n = (L . (G1 . n)) * (((G1 . n) |-- If) . x) ) )

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: ( G1 is one-to-one & rng G1 = Carrier L & ( for n being Nat st n in dom F1 holds

F1 . n = (L . (G1 . n)) * (((G1 . n) |-- If) . x) ) )

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: ( rng G1 = Carrier L & ( for n being Nat st n in dom F1 holds

F1 . n = (L . (G1 . n)) * (((G1 . n) |-- If) . x) ) )

thus rng G1 = (B \ {v}) \/ {v} by A40, A45, A50, FINSEQ_1:31

.= Carrier L by A7, A25, ZFMISC_1:116 ; :: thesis: for n being Nat st n in dom F1 holds

F1 . n = (L . (G1 . n)) * (((G1 . n) |-- If) . x)

let n be Nat; :: thesis: ( n in dom F1 implies F1 . n = (L . (G1 . n)) * (((G1 . n) |-- If) . x) )

assume A51: n in dom F1 ; :: thesis: F1 . n = (L . (G1 . n)) * (((G1 . n) |-- If) . x)

then A52: n <= len F1 by FINSEQ_3:25;

end;( L . v <> 1 & v in Carrier L )

proof

then consider v being Element of V such that
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: verum

end;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: verum

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 Element of V; :: thesis: ex F being FinSequence of REAL ex G being FinSequence of V st
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B \ {v} or x in Carrier (L - K) )

assume A36: x in B \ {v} ; :: thesis: x in Carrier (L - K)

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: verum

end;assume A36: x in B \ {v} ; :: thesis: x in Carrier (L - K)

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: verum

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

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: ex G being FinSequence of V st

( ((Sum L) |-- If) . x = Sum F1 & len G = len F1 & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F1 holds

F1 . n = (L . (G . n)) * (((G . n) |-- If) . x) ) )

take G1 = G ^ <*v*>; :: thesis: ( ((Sum L) |-- If) . x = Sum F1 & len G1 = len F1 & G1 is one-to-one & rng G1 = Carrier L & ( for n being Nat st n in dom F1 holds

F1 . n = (L . (G1 . n)) * (((G1 . n) |-- If) . x) ) )

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: ( len G1 = len F1 & G1 is one-to-one & rng G1 = Carrier L & ( for n being Nat st n in dom F1 holds

F1 . n = (L . (G1 . n)) * (((G1 . n) |-- If) . x) ) )

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: ( G1 is one-to-one & rng G1 = Carrier L & ( for n being Nat st n in dom F1 holds

F1 . n = (L . (G1 . n)) * (((G1 . n) |-- If) . x) ) )

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: ( rng G1 = Carrier L & ( for n being Nat st n in dom F1 holds

F1 . n = (L . (G1 . n)) * (((G1 . n) |-- If) . x) ) )

thus rng G1 = (B \ {v}) \/ {v} by A40, A45, A50, FINSEQ_1:31

.= Carrier L by A7, A25, ZFMISC_1:116 ; :: thesis: for n being Nat st n in dom F1 holds

F1 . n = (L . (G1 . n)) * (((G1 . n) |-- If) . x)

let n be Nat; :: thesis: ( n in dom F1 implies F1 . n = (L . (G1 . n)) * (((G1 . n) |-- If) . x) )

assume A51: n in dom F1 ; :: thesis: F1 . n = (L . (G1 . n)) * (((G1 . n) |-- If) . x)

then A52: n <= len F1 by FINSEQ_3:25;

per cases
( ( 1 <= n & n <= len F ) or n = (len F) + 1 )
by A49, A51, A52, FINSEQ_3:25, NAT_1:8;

end;

suppose A53:
( 1 <= n & n <= len F )
; :: thesis: F1 . n = (L . (G1 . n)) * (((G1 . n) |-- If) . x)

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: verum

end;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: verum

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

assume that

A60: Af c= conv If and

A61: sum L = 1 ; :: thesis: ( 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) ) ) ) )

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

proof

for m being Nat holds S
let B be finite Subset of V; :: thesis: ( card B = 0 & B c= conv If implies 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) ) ) ) ) )

assume that

A64: card B = 0 and

B c= conv If ; :: thesis: 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) ) ) ) )

let L be Linear_Combination of B; :: thesis: ( Carrier L = B & sum L = 1 implies ( 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) ) ) ) ) )

assume that

Carrier L = B and

A65: sum L = 1 ; :: thesis: ( 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) ) ) ) )

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: verum

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

assume that

A64: card B = 0 and

B c= conv If ; :: thesis: 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) ) ) ) )

let L be Linear_Combination of B; :: thesis: ( Carrier L = B & sum L = 1 implies ( 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) ) ) ) ) )

assume that

Carrier L = B and

A65: sum L = 1 ; :: thesis: ( 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) ) ) ) )

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: verum

then ( sum L = sum L1 & S

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: verum