let V be RealLinearSpace; :: thesis: for M being convex Subset of V

for N being Subset of V

for L being Linear_Combination of N st L is convex & N c= M holds

Sum L in M

let M be convex Subset of V; :: thesis: for N being Subset of V

for L being Linear_Combination of N st L is convex & N c= M holds

Sum L in M

let N be Subset of V; :: thesis: for L being Linear_Combination of N st L is convex & N c= M holds

Sum L in M

let L be Linear_Combination of N; :: thesis: ( L is convex & N c= M implies Sum L in M )

assume that

A1: L is convex and

A2: N c= M ; :: thesis: Sum L in M

consider F being FinSequence of the carrier of V such that

A3: F is one-to-one and

A4: rng F = Carrier L and

A5: ex f being FinSequence of REAL st

( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds

( f . n = L . (F . n) & f . n >= 0 ) ) ) by A1;

consider f being FinSequence of REAL such that

A6: len f = len F and

A7: Sum f = 1 and

A8: for n being Nat st n in dom f holds

( f . n = L . (F . n) & f . n >= 0 ) by A5;

not Carrier L, {} are_equipotent by A1, CARD_1:26, CONVEX1:21;

then A9: card (Carrier L) <> card {} by CARD_1:5;

then reconsider i = len F as non zero Element of NAT by A3, A4, FINSEQ_4:62;

A10: len (L (#) F) = len F by RLVECT_2:def 7;

defpred S_{1}[ Nat] means (1 / (Sum (mid (f,1,$1)))) * (Sum (mid ((L (#) F),1,$1))) in M;

A11: len (L (#) F) = len F by RLVECT_2:def 7;

A12: for k being non zero Nat st S_{1}[k] holds

S_{1}[k + 1]

then A73: len F >= 0 + 1 by NAT_1:13;

A74: S_{1}[1]
_{1}[k]
from NAT_1:sch 10(A74, A12);

then A86: (1 / (Sum (mid (f,1,i)))) * (Sum (mid ((L (#) F),1,i))) in M ;

Sum (mid (f,1,(len f))) = 1 by A6, A7, A73, FINSEQ_6:120;

then (1 / (Sum (mid (f,1,(len f))))) * (Sum (mid ((L (#) F),1,(len (L (#) F))))) = Sum (mid ((L (#) F),1,(len (L (#) F)))) by RLVECT_1:def 8

.= Sum (L (#) F) by A73, A10, FINSEQ_6:120 ;

hence Sum L in M by A3, A4, A6, A86, A10, RLVECT_2:def 8; :: thesis: verum

for N being Subset of V

for L being Linear_Combination of N st L is convex & N c= M holds

Sum L in M

let M be convex Subset of V; :: thesis: for N being Subset of V

for L being Linear_Combination of N st L is convex & N c= M holds

Sum L in M

let N be Subset of V; :: thesis: for L being Linear_Combination of N st L is convex & N c= M holds

Sum L in M

let L be Linear_Combination of N; :: thesis: ( L is convex & N c= M implies Sum L in M )

assume that

A1: L is convex and

A2: N c= M ; :: thesis: Sum L in M

consider F being FinSequence of the carrier of V such that

A3: F is one-to-one and

A4: rng F = Carrier L and

A5: ex f being FinSequence of REAL st

( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds

( f . n = L . (F . n) & f . n >= 0 ) ) ) by A1;

consider f being FinSequence of REAL such that

A6: len f = len F and

A7: Sum f = 1 and

A8: for n being Nat st n in dom f holds

( f . n = L . (F . n) & f . n >= 0 ) by A5;

not Carrier L, {} are_equipotent by A1, CARD_1:26, CONVEX1:21;

then A9: card (Carrier L) <> card {} by CARD_1:5;

then reconsider i = len F as non zero Element of NAT by A3, A4, FINSEQ_4:62;

A10: len (L (#) F) = len F by RLVECT_2:def 7;

defpred S

A11: len (L (#) F) = len F by RLVECT_2:def 7;

A12: for k being non zero Nat st S

S

proof

len F > 0
by A3, A4, A9, FINSEQ_4:62;
let k be non zero Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

A13: k >= 1 by NAT_1:14;

assume A14: (1 / (Sum (mid (f,1,k)))) * (Sum (mid ((L (#) F),1,k))) in M ; :: thesis: S_{1}[k + 1]

_{1}[k + 1]
; :: thesis: verum

end;A13: k >= 1 by NAT_1:14;

assume A14: (1 / (Sum (mid (f,1,k)))) * (Sum (mid ((L (#) F),1,k))) in M ; :: thesis: S

now :: thesis: S_{1}[k + 1]end;

hence
Sper cases
( k >= len f or k < len f )
;

end;

suppose A15:
k >= len f
; :: thesis: S_{1}[k + 1]

A16: mid ((L (#) F),1,(k + 1)) =
(L (#) F) | (k + 1)
by FINSEQ_6:116, NAT_1:12

.= L (#) F by A6, A11, A15, FINSEQ_1:58, NAT_1:12 ;

A17: mid (f,1,k) = f | k by FINSEQ_6:116, NAT_1:14

.= f by A15, FINSEQ_1:58 ;

A18: mid (f,1,(k + 1)) = f | (k + 1) by FINSEQ_6:116, NAT_1:12

.= f by A15, FINSEQ_1:58, NAT_1:12 ;

mid ((L (#) F),1,k) = (L (#) F) | k by FINSEQ_6:116, NAT_1:14

.= L (#) F by A6, A11, A15, FINSEQ_1:58 ;

hence S_{1}[k + 1]
by A14, A17, A18, A16; :: thesis: verum

end;.= L (#) F by A6, A11, A15, FINSEQ_1:58, NAT_1:12 ;

A17: mid (f,1,k) = f | k by FINSEQ_6:116, NAT_1:14

.= f by A15, FINSEQ_1:58 ;

A18: mid (f,1,(k + 1)) = f | (k + 1) by FINSEQ_6:116, NAT_1:12

.= f by A15, FINSEQ_1:58, NAT_1:12 ;

mid ((L (#) F),1,k) = (L (#) F) | k by FINSEQ_6:116, NAT_1:14

.= L (#) F by A6, A11, A15, FINSEQ_1:58 ;

hence S

suppose A19:
k < len f
; :: thesis: S_{1}[k + 1]

mid (f,1,k) = f | k
by FINSEQ_6:116, NAT_1:14;

then A20: len (mid (f,1,k)) = k by A19, FINSEQ_1:59;

A21: ex i being Element of NAT st

( i in dom (mid (f,1,k)) & 0 < (mid (f,1,k)) . i )

(mid (f,1,(k + 1))) . ((len (mid (f,1,k))) + i) = <*((mid (f,1,(k + 1))) . (k + 1))*> . i

set r1 = Sum (mid (f,1,k));

for i being Nat st i in dom (mid (f,1,k)) holds

0 <= (mid (f,1,k)) . i

A32: k + 1 <= len f by A19, NAT_1:13;

then A33: len (f | (k + 1)) = k + 1 by FINSEQ_1:59;

A34: for i being Nat st i in dom (mid (f,1,k)) holds

(mid (f,1,(k + 1))) . i = (mid (f,1,k)) . i

then A42: k + 1 in Seg (len f) by A32;

then A43: k + 1 in dom f by FINSEQ_1:def 3;

A44: k + 1 in dom F by A6, A42, FINSEQ_1:def 3;

k + 1 in Seg (k + 1) by A41;

then A45: k + 1 in dom (f | (k + 1)) by A33, FINSEQ_1:def 3;

then (f | (k + 1)) /. (k + 1) = f /. (k + 1) by FINSEQ_4:70;

then (mid (f,1,(k + 1))) . (k + 1) = f /. (k + 1) by A26, A45, PARTFUN1:def 6;

then (mid (f,1,(k + 1))) . (k + 1) = f . (k + 1) by A43, PARTFUN1:def 6

.= L . (F . (k + 1)) by A8, A43 ;

then A46: (mid (f,1,(k + 1))) . (k + 1) = L . (F /. (k + 1)) by A44, PARTFUN1:def 6;

mid (f,1,(k + 1)) = f | (k + 1) by FINSEQ_6:116, NAT_1:14;

then ( len <*((mid (f,1,(k + 1))) . (k + 1))*> = 1 & len (mid (f,1,(k + 1))) = k + 1 ) by A32, FINSEQ_1:40, FINSEQ_1:59;

then dom (mid (f,1,(k + 1))) = Seg ((len (mid (f,1,k))) + (len <*((mid (f,1,(k + 1))) . (k + 1))*>)) by A20, FINSEQ_1:def 3;

then mid (f,1,(k + 1)) = (mid (f,1,k)) ^ <*((mid (f,1,(k + 1))) . (k + 1))*> by A34, A25, FINSEQ_1:def 7;

then A47: Sum (mid (f,1,(k + 1))) = (Sum (mid (f,1,k))) + (L . (F /. (k + 1))) by A46, RVSUM_1:74;

A48: mid ((L (#) F),1,(k + 1)) = (L (#) F) | (k + 1) by FINSEQ_6:116, NAT_1:14;

set w2 = F /. (k + 1);

set w1 = Sum (mid ((L (#) F),1,k));

set r2 = L . (F /. (k + 1));

A49: (1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * (Sum (mid (f,1,k))) = (Sum (mid (f,1,k))) / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1)))) by XCMPLX_1:99;

A50: ( F /. (k + 1) in M & L . (F /. (k + 1)) > 0 )

then A54: (1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * (Sum (mid (f,1,k))) < 1 by A31, A49, XREAL_1:189;

A55: (Sum (mid (f,1,k))) + (L . (F /. (k + 1))) > 0 + 0 by A31, A50;

then 1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1)))) > 0 by XREAL_1:139;

then A56: 0 < (1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * (Sum (mid (f,1,k))) by A31, XREAL_1:129;

k + 1 <= len (L (#) F) by A6, A32, RLVECT_2:def 7;

then A57: k + 1 in dom (L (#) F) by A41, FINSEQ_3:25;

A58: k < len (L (#) F) by A6, A19, RLVECT_2:def 7;

then A59: k + 1 <= len (L (#) F) by NAT_1:13;

then A60: len ((L (#) F) | (k + 1)) = k + 1 by FINSEQ_1:59;

A61: for i being Nat st i in dom (mid ((L (#) F),1,k)) holds

(mid ((L (#) F),1,(k + 1))) . i = (mid ((L (#) F),1,k)) . i

then A68: k + 1 in dom ((L (#) F) | (k + 1)) by A60, FINSEQ_1:def 3;

then ((L (#) F) | (k + 1)) /. (k + 1) = (L (#) F) /. (k + 1) by FINSEQ_4:70;

then (mid ((L (#) F),1,(k + 1))) . (k + 1) = (L (#) F) /. (k + 1) by A48, A68, PARTFUN1:def 6;

then A69: (mid ((L (#) F),1,(k + 1))) . (k + 1) = (L (#) F) . (k + 1) by A57, PARTFUN1:def 6

.= (L . (F /. (k + 1))) * (F /. (k + 1)) by A57, RLVECT_2:def 7 ;

mid ((L (#) F),1,k) = (L (#) F) | k by FINSEQ_6:116, NAT_1:14;

then A70: len (mid ((L (#) F),1,k)) = k by A58, FINSEQ_1:59;

A71: for i being Nat st i in dom <*((mid ((L (#) F),1,(k + 1))) . (k + 1))*> holds

(mid ((L (#) F),1,(k + 1))) . ((len (mid ((L (#) F),1,k))) + i) = <*((mid ((L (#) F),1,(k + 1))) . (k + 1))*> . i

then dom (mid ((L (#) F),1,(k + 1))) = Seg ((len (mid ((L (#) F),1,k))) + (len <*((mid ((L (#) F),1,(k + 1))) . (k + 1))*>)) by A70, FINSEQ_1:def 3;

then mid ((L (#) F),1,(k + 1)) = (mid ((L (#) F),1,k)) ^ <*((mid ((L (#) F),1,(k + 1))) . (k + 1))*> by A61, A71, FINSEQ_1:def 7;

then A72: (1 / (Sum (mid (f,1,(k + 1))))) * (Sum (mid ((L (#) F),1,(k + 1)))) = (1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * ((Sum (mid ((L (#) F),1,k))) + ((L . (F /. (k + 1))) * (F /. (k + 1)))) by A47, A69, FVSUM_1:71

.= (1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * ((1 * (Sum (mid ((L (#) F),1,k)))) + ((L . (F /. (k + 1))) * (F /. (k + 1)))) by RLVECT_1:def 8

.= (1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * ((((Sum (mid (f,1,k))) * (1 / (Sum (mid (f,1,k))))) * (Sum (mid ((L (#) F),1,k)))) + ((L . (F /. (k + 1))) * (F /. (k + 1)))) by A31, XCMPLX_1:106

.= (1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * (((Sum (mid (f,1,k))) * ((1 / (Sum (mid (f,1,k)))) * (Sum (mid ((L (#) F),1,k))))) + ((L . (F /. (k + 1))) * (F /. (k + 1)))) by RLVECT_1:def 7

.= ((1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * ((Sum (mid (f,1,k))) * ((1 / (Sum (mid (f,1,k)))) * (Sum (mid ((L (#) F),1,k)))))) + ((1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * ((L . (F /. (k + 1))) * (F /. (k + 1)))) by RLVECT_1:def 5

.= (((1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * (Sum (mid (f,1,k)))) * ((1 / (Sum (mid (f,1,k)))) * (Sum (mid ((L (#) F),1,k))))) + ((1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * ((L . (F /. (k + 1))) * (F /. (k + 1)))) by RLVECT_1:def 7

.= (((1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * (Sum (mid (f,1,k)))) * ((1 / (Sum (mid (f,1,k)))) * (Sum (mid ((L (#) F),1,k))))) + (((1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * (L . (F /. (k + 1)))) * (F /. (k + 1))) by RLVECT_1:def 7 ;

1 - ((1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * (Sum (mid (f,1,k)))) = (((Sum (mid (f,1,k))) + (L . (F /. (k + 1)))) * (1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1)))))) - ((1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * (Sum (mid (f,1,k)))) by A55, XCMPLX_1:106

.= (((Sum (mid (f,1,k))) + (L . (F /. (k + 1)))) - (Sum (mid (f,1,k)))) * (1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) ;

hence S_{1}[k + 1]
by A14, A50, A56, A54, A72, CONVEX1:def 2; :: thesis: verum

end;then A20: len (mid (f,1,k)) = k by A19, FINSEQ_1:59;

A21: ex i being Element of NAT st

( i in dom (mid (f,1,k)) & 0 < (mid (f,1,k)) . i )

proof

A25:
for i being Nat st i in dom <*((mid (f,1,(k + 1))) . (k + 1))*> holds
take
1
; :: thesis: ( 1 in dom (mid (f,1,k)) & 0 < (mid (f,1,k)) . 1 )

1 <= len f by A19, NAT_1:14;

then A22: 1 in Seg (len f) ;

then 1 in dom f by FINSEQ_1:def 3;

then A23: ( f . 1 = L . (F . 1) & f . 1 >= 0 ) by A8;

1 in dom F by A6, A22, FINSEQ_1:def 3;

then F . 1 in Carrier L by A4, FUNCT_1:def 3;

then F . 1 in { v where v is Element of V : L . v <> 0 } by RLVECT_2:def 4;

then A24: ex v being Element of V st

( v = F . 1 & L . v <> 0 ) ;

1 in Seg (len (mid (f,1,k))) by A13, A20;

hence ( 1 in dom (mid (f,1,k)) & 0 < (mid (f,1,k)) . 1 ) by A13, A19, A23, A24, FINSEQ_1:def 3, FINSEQ_6:123; :: thesis: verum

end;1 <= len f by A19, NAT_1:14;

then A22: 1 in Seg (len f) ;

then 1 in dom f by FINSEQ_1:def 3;

then A23: ( f . 1 = L . (F . 1) & f . 1 >= 0 ) by A8;

1 in dom F by A6, A22, FINSEQ_1:def 3;

then F . 1 in Carrier L by A4, FUNCT_1:def 3;

then F . 1 in { v where v is Element of V : L . v <> 0 } by RLVECT_2:def 4;

then A24: ex v being Element of V st

( v = F . 1 & L . v <> 0 ) ;

1 in Seg (len (mid (f,1,k))) by A13, A20;

hence ( 1 in dom (mid (f,1,k)) & 0 < (mid (f,1,k)) . 1 ) by A13, A19, A23, A24, FINSEQ_1:def 3, FINSEQ_6:123; :: thesis: verum

(mid (f,1,(k + 1))) . ((len (mid (f,1,k))) + i) = <*((mid (f,1,(k + 1))) . (k + 1))*> . i

proof

A26:
mid (f,1,(k + 1)) = f | (k + 1)
by FINSEQ_6:116, NAT_1:14;
let i be Nat; :: thesis: ( i in dom <*((mid (f,1,(k + 1))) . (k + 1))*> implies (mid (f,1,(k + 1))) . ((len (mid (f,1,k))) + i) = <*((mid (f,1,(k + 1))) . (k + 1))*> . i )

assume i in dom <*((mid (f,1,(k + 1))) . (k + 1))*> ; :: thesis: (mid (f,1,(k + 1))) . ((len (mid (f,1,k))) + i) = <*((mid (f,1,(k + 1))) . (k + 1))*> . i

then i in Seg 1 by FINSEQ_1:38;

then i = 1 by FINSEQ_1:2, TARSKI:def 1;

hence (mid (f,1,(k + 1))) . ((len (mid (f,1,k))) + i) = <*((mid (f,1,(k + 1))) . (k + 1))*> . i by A20, FINSEQ_1:40; :: thesis: verum

end;assume i in dom <*((mid (f,1,(k + 1))) . (k + 1))*> ; :: thesis: (mid (f,1,(k + 1))) . ((len (mid (f,1,k))) + i) = <*((mid (f,1,(k + 1))) . (k + 1))*> . i

then i in Seg 1 by FINSEQ_1:38;

then i = 1 by FINSEQ_1:2, TARSKI:def 1;

hence (mid (f,1,(k + 1))) . ((len (mid (f,1,k))) + i) = <*((mid (f,1,(k + 1))) . (k + 1))*> . i by A20, FINSEQ_1:40; :: thesis: verum

set r1 = Sum (mid (f,1,k));

for i being Nat st i in dom (mid (f,1,k)) holds

0 <= (mid (f,1,k)) . i

proof

then A31:
Sum (mid (f,1,k)) > 0
by A21, RVSUM_1:85;
let i be Nat; :: thesis: ( i in dom (mid (f,1,k)) implies 0 <= (mid (f,1,k)) . i )

assume i in dom (mid (f,1,k)) ; :: thesis: 0 <= (mid (f,1,k)) . i

then A27: i in Seg k by A20, FINSEQ_1:def 3;

then A28: 1 <= i by FINSEQ_1:1;

A29: i <= k by A27, FINSEQ_1:1;

then i <= len f by A19, XXREAL_0:2;

then A30: i in dom f by A28, FINSEQ_3:25;

(mid (f,1,k)) . i = f . i by A19, A28, A29, FINSEQ_6:123;

hence 0 <= (mid (f,1,k)) . i by A8, A30; :: thesis: verum

end;assume i in dom (mid (f,1,k)) ; :: thesis: 0 <= (mid (f,1,k)) . i

then A27: i in Seg k by A20, FINSEQ_1:def 3;

then A28: 1 <= i by FINSEQ_1:1;

A29: i <= k by A27, FINSEQ_1:1;

then i <= len f by A19, XXREAL_0:2;

then A30: i in dom f by A28, FINSEQ_3:25;

(mid (f,1,k)) . i = f . i by A19, A28, A29, FINSEQ_6:123;

hence 0 <= (mid (f,1,k)) . i by A8, A30; :: thesis: verum

A32: k + 1 <= len f by A19, NAT_1:13;

then A33: len (f | (k + 1)) = k + 1 by FINSEQ_1:59;

A34: for i being Nat st i in dom (mid (f,1,k)) holds

(mid (f,1,(k + 1))) . i = (mid (f,1,k)) . i

proof

A41:
k + 1 >= 1
by NAT_1:14;
let i be Nat; :: thesis: ( i in dom (mid (f,1,k)) implies (mid (f,1,(k + 1))) . i = (mid (f,1,k)) . i )

A35: mid (f,1,k) = f | k by FINSEQ_6:116, NAT_1:14;

assume A36: i in dom (mid (f,1,k)) ; :: thesis: (mid (f,1,(k + 1))) . i = (mid (f,1,k)) . i

then A37: i in Seg (len (f | k)) by A35, FINSEQ_1:def 3;

len (f | k) = k by A19, FINSEQ_1:59;

then i <= k by A37, FINSEQ_1:1;

then A38: i <= k + 1 by NAT_1:12;

(f | k) . i = (f | k) /. i by A36, A35, PARTFUN1:def 6;

then A39: (mid (f,1,k)) . i = f /. i by A36, A35, FINSEQ_4:70;

( i in NAT & 1 <= i ) by A37, FINSEQ_1:1;

then i in Seg (k + 1) by A38;

then A40: i in dom (f | (k + 1)) by A33, FINSEQ_1:def 3;

then (f | (k + 1)) . i = (f | (k + 1)) /. i by PARTFUN1:def 6;

hence (mid (f,1,(k + 1))) . i = (mid (f,1,k)) . i by A26, A39, A40, FINSEQ_4:70; :: thesis: verum

end;A35: mid (f,1,k) = f | k by FINSEQ_6:116, NAT_1:14;

assume A36: i in dom (mid (f,1,k)) ; :: thesis: (mid (f,1,(k + 1))) . i = (mid (f,1,k)) . i

then A37: i in Seg (len (f | k)) by A35, FINSEQ_1:def 3;

len (f | k) = k by A19, FINSEQ_1:59;

then i <= k by A37, FINSEQ_1:1;

then A38: i <= k + 1 by NAT_1:12;

(f | k) . i = (f | k) /. i by A36, A35, PARTFUN1:def 6;

then A39: (mid (f,1,k)) . i = f /. i by A36, A35, FINSEQ_4:70;

( i in NAT & 1 <= i ) by A37, FINSEQ_1:1;

then i in Seg (k + 1) by A38;

then A40: i in dom (f | (k + 1)) by A33, FINSEQ_1:def 3;

then (f | (k + 1)) . i = (f | (k + 1)) /. i by PARTFUN1:def 6;

hence (mid (f,1,(k + 1))) . i = (mid (f,1,k)) . i by A26, A39, A40, FINSEQ_4:70; :: thesis: verum

then A42: k + 1 in Seg (len f) by A32;

then A43: k + 1 in dom f by FINSEQ_1:def 3;

A44: k + 1 in dom F by A6, A42, FINSEQ_1:def 3;

k + 1 in Seg (k + 1) by A41;

then A45: k + 1 in dom (f | (k + 1)) by A33, FINSEQ_1:def 3;

then (f | (k + 1)) /. (k + 1) = f /. (k + 1) by FINSEQ_4:70;

then (mid (f,1,(k + 1))) . (k + 1) = f /. (k + 1) by A26, A45, PARTFUN1:def 6;

then (mid (f,1,(k + 1))) . (k + 1) = f . (k + 1) by A43, PARTFUN1:def 6

.= L . (F . (k + 1)) by A8, A43 ;

then A46: (mid (f,1,(k + 1))) . (k + 1) = L . (F /. (k + 1)) by A44, PARTFUN1:def 6;

mid (f,1,(k + 1)) = f | (k + 1) by FINSEQ_6:116, NAT_1:14;

then ( len <*((mid (f,1,(k + 1))) . (k + 1))*> = 1 & len (mid (f,1,(k + 1))) = k + 1 ) by A32, FINSEQ_1:40, FINSEQ_1:59;

then dom (mid (f,1,(k + 1))) = Seg ((len (mid (f,1,k))) + (len <*((mid (f,1,(k + 1))) . (k + 1))*>)) by A20, FINSEQ_1:def 3;

then mid (f,1,(k + 1)) = (mid (f,1,k)) ^ <*((mid (f,1,(k + 1))) . (k + 1))*> by A34, A25, FINSEQ_1:def 7;

then A47: Sum (mid (f,1,(k + 1))) = (Sum (mid (f,1,k))) + (L . (F /. (k + 1))) by A46, RVSUM_1:74;

A48: mid ((L (#) F),1,(k + 1)) = (L (#) F) | (k + 1) by FINSEQ_6:116, NAT_1:14;

set w2 = F /. (k + 1);

set w1 = Sum (mid ((L (#) F),1,k));

set r2 = L . (F /. (k + 1));

A49: (1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * (Sum (mid (f,1,k))) = (Sum (mid (f,1,k))) / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1)))) by XCMPLX_1:99;

A50: ( F /. (k + 1) in M & L . (F /. (k + 1)) > 0 )

proof

then
(Sum (mid (f,1,k))) + (L . (F /. (k + 1))) > Sum (mid (f,1,k))
by XREAL_1:29;
k + 1 in Seg (len f)
by A41, A32;

then k + 1 in dom f by FINSEQ_1:def 3;

then A51: ( f . (k + 1) = L . (F . (k + 1)) & f . (k + 1) >= 0 ) by A8;

k + 1 in Seg (len F) by A6, A41, A32;

then A52: k + 1 in dom F by FINSEQ_1:def 3;

then F /. (k + 1) = F . (k + 1) by PARTFUN1:def 6;

then A53: F /. (k + 1) in Carrier L by A4, A52, FUNCT_1:def 3;

Carrier L c= N by RLVECT_2:def 6;

hence F /. (k + 1) in M by A2, A53; :: thesis: L . (F /. (k + 1)) > 0

F /. (k + 1) in { v where v is Element of V : L . v <> 0 } by A53, RLVECT_2:def 4;

then ex v being Element of V st

( v = F /. (k + 1) & L . v <> 0 ) ;

hence L . (F /. (k + 1)) > 0 by A52, A51, PARTFUN1:def 6; :: thesis: verum

end;then k + 1 in dom f by FINSEQ_1:def 3;

then A51: ( f . (k + 1) = L . (F . (k + 1)) & f . (k + 1) >= 0 ) by A8;

k + 1 in Seg (len F) by A6, A41, A32;

then A52: k + 1 in dom F by FINSEQ_1:def 3;

then F /. (k + 1) = F . (k + 1) by PARTFUN1:def 6;

then A53: F /. (k + 1) in Carrier L by A4, A52, FUNCT_1:def 3;

Carrier L c= N by RLVECT_2:def 6;

hence F /. (k + 1) in M by A2, A53; :: thesis: L . (F /. (k + 1)) > 0

F /. (k + 1) in { v where v is Element of V : L . v <> 0 } by A53, RLVECT_2:def 4;

then ex v being Element of V st

( v = F /. (k + 1) & L . v <> 0 ) ;

hence L . (F /. (k + 1)) > 0 by A52, A51, PARTFUN1:def 6; :: thesis: verum

then A54: (1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * (Sum (mid (f,1,k))) < 1 by A31, A49, XREAL_1:189;

A55: (Sum (mid (f,1,k))) + (L . (F /. (k + 1))) > 0 + 0 by A31, A50;

then 1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1)))) > 0 by XREAL_1:139;

then A56: 0 < (1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * (Sum (mid (f,1,k))) by A31, XREAL_1:129;

k + 1 <= len (L (#) F) by A6, A32, RLVECT_2:def 7;

then A57: k + 1 in dom (L (#) F) by A41, FINSEQ_3:25;

A58: k < len (L (#) F) by A6, A19, RLVECT_2:def 7;

then A59: k + 1 <= len (L (#) F) by NAT_1:13;

then A60: len ((L (#) F) | (k + 1)) = k + 1 by FINSEQ_1:59;

A61: for i being Nat st i in dom (mid ((L (#) F),1,k)) holds

(mid ((L (#) F),1,(k + 1))) . i = (mid ((L (#) F),1,k)) . i

proof

k + 1 in Seg (k + 1)
by A41;
let i be Nat; :: thesis: ( i in dom (mid ((L (#) F),1,k)) implies (mid ((L (#) F),1,(k + 1))) . i = (mid ((L (#) F),1,k)) . i )

A62: mid ((L (#) F),1,k) = (L (#) F) | k by FINSEQ_6:116, NAT_1:14;

assume A63: i in dom (mid ((L (#) F),1,k)) ; :: thesis: (mid ((L (#) F),1,(k + 1))) . i = (mid ((L (#) F),1,k)) . i

then A64: i in Seg (len ((L (#) F) | k)) by A62, FINSEQ_1:def 3;

len ((L (#) F) | k) = k by A58, FINSEQ_1:59;

then i <= k by A64, FINSEQ_1:1;

then A65: i <= k + 1 by NAT_1:12;

((L (#) F) | k) . i = ((L (#) F) | k) /. i by A63, A62, PARTFUN1:def 6;

then A66: (mid ((L (#) F),1,k)) . i = (L (#) F) /. i by A63, A62, FINSEQ_4:70;

( i in NAT & 1 <= i ) by A64, FINSEQ_1:1;

then i in Seg (k + 1) by A65;

then A67: i in dom ((L (#) F) | (k + 1)) by A60, FINSEQ_1:def 3;

then ((L (#) F) | (k + 1)) . i = ((L (#) F) | (k + 1)) /. i by PARTFUN1:def 6;

hence (mid ((L (#) F),1,(k + 1))) . i = (mid ((L (#) F),1,k)) . i by A48, A66, A67, FINSEQ_4:70; :: thesis: verum

end;A62: mid ((L (#) F),1,k) = (L (#) F) | k by FINSEQ_6:116, NAT_1:14;

assume A63: i in dom (mid ((L (#) F),1,k)) ; :: thesis: (mid ((L (#) F),1,(k + 1))) . i = (mid ((L (#) F),1,k)) . i

then A64: i in Seg (len ((L (#) F) | k)) by A62, FINSEQ_1:def 3;

len ((L (#) F) | k) = k by A58, FINSEQ_1:59;

then i <= k by A64, FINSEQ_1:1;

then A65: i <= k + 1 by NAT_1:12;

((L (#) F) | k) . i = ((L (#) F) | k) /. i by A63, A62, PARTFUN1:def 6;

then A66: (mid ((L (#) F),1,k)) . i = (L (#) F) /. i by A63, A62, FINSEQ_4:70;

( i in NAT & 1 <= i ) by A64, FINSEQ_1:1;

then i in Seg (k + 1) by A65;

then A67: i in dom ((L (#) F) | (k + 1)) by A60, FINSEQ_1:def 3;

then ((L (#) F) | (k + 1)) . i = ((L (#) F) | (k + 1)) /. i by PARTFUN1:def 6;

hence (mid ((L (#) F),1,(k + 1))) . i = (mid ((L (#) F),1,k)) . i by A48, A66, A67, FINSEQ_4:70; :: thesis: verum

then A68: k + 1 in dom ((L (#) F) | (k + 1)) by A60, FINSEQ_1:def 3;

then ((L (#) F) | (k + 1)) /. (k + 1) = (L (#) F) /. (k + 1) by FINSEQ_4:70;

then (mid ((L (#) F),1,(k + 1))) . (k + 1) = (L (#) F) /. (k + 1) by A48, A68, PARTFUN1:def 6;

then A69: (mid ((L (#) F),1,(k + 1))) . (k + 1) = (L (#) F) . (k + 1) by A57, PARTFUN1:def 6

.= (L . (F /. (k + 1))) * (F /. (k + 1)) by A57, RLVECT_2:def 7 ;

mid ((L (#) F),1,k) = (L (#) F) | k by FINSEQ_6:116, NAT_1:14;

then A70: len (mid ((L (#) F),1,k)) = k by A58, FINSEQ_1:59;

A71: for i being Nat st i in dom <*((mid ((L (#) F),1,(k + 1))) . (k + 1))*> holds

(mid ((L (#) F),1,(k + 1))) . ((len (mid ((L (#) F),1,k))) + i) = <*((mid ((L (#) F),1,(k + 1))) . (k + 1))*> . i

proof

( len <*((mid ((L (#) F),1,(k + 1))) . (k + 1))*> = 1 & len (mid ((L (#) F),1,(k + 1))) = k + 1 )
by A59, A48, FINSEQ_1:40, FINSEQ_1:59;
let i be Nat; :: thesis: ( i in dom <*((mid ((L (#) F),1,(k + 1))) . (k + 1))*> implies (mid ((L (#) F),1,(k + 1))) . ((len (mid ((L (#) F),1,k))) + i) = <*((mid ((L (#) F),1,(k + 1))) . (k + 1))*> . i )

assume i in dom <*((mid ((L (#) F),1,(k + 1))) . (k + 1))*> ; :: thesis: (mid ((L (#) F),1,(k + 1))) . ((len (mid ((L (#) F),1,k))) + i) = <*((mid ((L (#) F),1,(k + 1))) . (k + 1))*> . i

then i in Seg 1 by FINSEQ_1:38;

then i = 1 by FINSEQ_1:2, TARSKI:def 1;

hence (mid ((L (#) F),1,(k + 1))) . ((len (mid ((L (#) F),1,k))) + i) = <*((mid ((L (#) F),1,(k + 1))) . (k + 1))*> . i by A70, FINSEQ_1:40; :: thesis: verum

end;assume i in dom <*((mid ((L (#) F),1,(k + 1))) . (k + 1))*> ; :: thesis: (mid ((L (#) F),1,(k + 1))) . ((len (mid ((L (#) F),1,k))) + i) = <*((mid ((L (#) F),1,(k + 1))) . (k + 1))*> . i

then i in Seg 1 by FINSEQ_1:38;

then i = 1 by FINSEQ_1:2, TARSKI:def 1;

hence (mid ((L (#) F),1,(k + 1))) . ((len (mid ((L (#) F),1,k))) + i) = <*((mid ((L (#) F),1,(k + 1))) . (k + 1))*> . i by A70, FINSEQ_1:40; :: thesis: verum

then dom (mid ((L (#) F),1,(k + 1))) = Seg ((len (mid ((L (#) F),1,k))) + (len <*((mid ((L (#) F),1,(k + 1))) . (k + 1))*>)) by A70, FINSEQ_1:def 3;

then mid ((L (#) F),1,(k + 1)) = (mid ((L (#) F),1,k)) ^ <*((mid ((L (#) F),1,(k + 1))) . (k + 1))*> by A61, A71, FINSEQ_1:def 7;

then A72: (1 / (Sum (mid (f,1,(k + 1))))) * (Sum (mid ((L (#) F),1,(k + 1)))) = (1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * ((Sum (mid ((L (#) F),1,k))) + ((L . (F /. (k + 1))) * (F /. (k + 1)))) by A47, A69, FVSUM_1:71

.= (1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * ((1 * (Sum (mid ((L (#) F),1,k)))) + ((L . (F /. (k + 1))) * (F /. (k + 1)))) by RLVECT_1:def 8

.= (1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * ((((Sum (mid (f,1,k))) * (1 / (Sum (mid (f,1,k))))) * (Sum (mid ((L (#) F),1,k)))) + ((L . (F /. (k + 1))) * (F /. (k + 1)))) by A31, XCMPLX_1:106

.= (1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * (((Sum (mid (f,1,k))) * ((1 / (Sum (mid (f,1,k)))) * (Sum (mid ((L (#) F),1,k))))) + ((L . (F /. (k + 1))) * (F /. (k + 1)))) by RLVECT_1:def 7

.= ((1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * ((Sum (mid (f,1,k))) * ((1 / (Sum (mid (f,1,k)))) * (Sum (mid ((L (#) F),1,k)))))) + ((1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * ((L . (F /. (k + 1))) * (F /. (k + 1)))) by RLVECT_1:def 5

.= (((1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * (Sum (mid (f,1,k)))) * ((1 / (Sum (mid (f,1,k)))) * (Sum (mid ((L (#) F),1,k))))) + ((1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * ((L . (F /. (k + 1))) * (F /. (k + 1)))) by RLVECT_1:def 7

.= (((1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * (Sum (mid (f,1,k)))) * ((1 / (Sum (mid (f,1,k)))) * (Sum (mid ((L (#) F),1,k))))) + (((1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * (L . (F /. (k + 1)))) * (F /. (k + 1))) by RLVECT_1:def 7 ;

1 - ((1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * (Sum (mid (f,1,k)))) = (((Sum (mid (f,1,k))) + (L . (F /. (k + 1)))) * (1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1)))))) - ((1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * (Sum (mid (f,1,k)))) by A55, XCMPLX_1:106

.= (((Sum (mid (f,1,k))) + (L . (F /. (k + 1)))) - (Sum (mid (f,1,k)))) * (1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) ;

hence S

then A73: len F >= 0 + 1 by NAT_1:13;

A74: S

proof

for k being non zero Nat holds S
mid (f,1,1) = f | 1
by FINSEQ_6:116;

then A75: len (mid (f,1,1)) = 1 by A6, A73, FINSEQ_1:59;

then 1 in dom (mid (f,1,1)) by FINSEQ_3:25;

then reconsider m = (mid (f,1,1)) . 1 as Element of REAL by PARTFUN1:4;

mid (f,1,1) = <*((mid (f,1,1)) . 1)*> by A75, FINSEQ_1:40;

then A76: Sum (mid (f,1,1)) = m by FINSOP_1:11;

Carrier L c= N by RLVECT_2:def 6;

then A77: Carrier L c= M by A2;

mid ((L (#) F),1,1) = (L (#) F) | 1 by FINSEQ_6:116;

then len (mid ((L (#) F),1,1)) = 1 by A73, A11, FINSEQ_1:59;

then A78: mid ((L (#) F),1,1) = <*((mid ((L (#) F),1,1)) . 1)*> by FINSEQ_1:40;

A79: 1 in Seg (len (L (#) F)) by A73, A11;

then A80: 1 in dom F by A11, FINSEQ_1:def 3;

then A81: F /. 1 = F . 1 by PARTFUN1:def 6;

A82: 1 in dom (L (#) F) by A79, FINSEQ_1:def 3;

A83: F . 1 in rng F by A80, FUNCT_1:def 3;

then F . 1 in { v where v is Element of V : L . v <> 0 } by A4, RLVECT_2:def 4;

then A84: ex v2 being Element of V st

( F . 1 = v2 & L . v2 <> 0 ) ;

1 in dom f by A6, A11, A79, FINSEQ_1:def 3;

then f . 1 = L . (F . 1) by A8

.= L . (F /. 1) by A80, PARTFUN1:def 6 ;

then A85: Sum (mid (f,1,1)) = L . (F /. 1) by A6, A73, A76, FINSEQ_6:123;

(mid ((L (#) F),1,1)) . 1 = (L (#) F) . 1 by A73, A11, FINSEQ_6:123

.= (L . (F /. 1)) * (F /. 1) by A82, RLVECT_2:def 7 ;

then (1 / (Sum (mid (f,1,1)))) * (Sum (mid ((L (#) F),1,1))) = (1 / (Sum (mid (f,1,1)))) * ((L . (F /. 1)) * (F /. 1)) by A78, RLVECT_1:44

.= ((1 / (Sum (mid (f,1,1)))) * (L . (F /. 1))) * (F /. 1) by RLVECT_1:def 7

.= 1 * (F /. 1) by A81, A85, A84, XCMPLX_1:106

.= F /. 1 by RLVECT_1:def 8 ;

hence S_{1}[1]
by A4, A81, A83, A77; :: thesis: verum

end;then A75: len (mid (f,1,1)) = 1 by A6, A73, FINSEQ_1:59;

then 1 in dom (mid (f,1,1)) by FINSEQ_3:25;

then reconsider m = (mid (f,1,1)) . 1 as Element of REAL by PARTFUN1:4;

mid (f,1,1) = <*((mid (f,1,1)) . 1)*> by A75, FINSEQ_1:40;

then A76: Sum (mid (f,1,1)) = m by FINSOP_1:11;

Carrier L c= N by RLVECT_2:def 6;

then A77: Carrier L c= M by A2;

mid ((L (#) F),1,1) = (L (#) F) | 1 by FINSEQ_6:116;

then len (mid ((L (#) F),1,1)) = 1 by A73, A11, FINSEQ_1:59;

then A78: mid ((L (#) F),1,1) = <*((mid ((L (#) F),1,1)) . 1)*> by FINSEQ_1:40;

A79: 1 in Seg (len (L (#) F)) by A73, A11;

then A80: 1 in dom F by A11, FINSEQ_1:def 3;

then A81: F /. 1 = F . 1 by PARTFUN1:def 6;

A82: 1 in dom (L (#) F) by A79, FINSEQ_1:def 3;

A83: F . 1 in rng F by A80, FUNCT_1:def 3;

then F . 1 in { v where v is Element of V : L . v <> 0 } by A4, RLVECT_2:def 4;

then A84: ex v2 being Element of V st

( F . 1 = v2 & L . v2 <> 0 ) ;

1 in dom f by A6, A11, A79, FINSEQ_1:def 3;

then f . 1 = L . (F . 1) by A8

.= L . (F /. 1) by A80, PARTFUN1:def 6 ;

then A85: Sum (mid (f,1,1)) = L . (F /. 1) by A6, A73, A76, FINSEQ_6:123;

(mid ((L (#) F),1,1)) . 1 = (L (#) F) . 1 by A73, A11, FINSEQ_6:123

.= (L . (F /. 1)) * (F /. 1) by A82, RLVECT_2:def 7 ;

then (1 / (Sum (mid (f,1,1)))) * (Sum (mid ((L (#) F),1,1))) = (1 / (Sum (mid (f,1,1)))) * ((L . (F /. 1)) * (F /. 1)) by A78, RLVECT_1:44

.= ((1 / (Sum (mid (f,1,1)))) * (L . (F /. 1))) * (F /. 1) by RLVECT_1:def 7

.= 1 * (F /. 1) by A81, A85, A84, XCMPLX_1:106

.= F /. 1 by RLVECT_1:def 8 ;

hence S

then A86: (1 / (Sum (mid (f,1,i)))) * (Sum (mid ((L (#) F),1,i))) in M ;

Sum (mid (f,1,(len f))) = 1 by A6, A7, A73, FINSEQ_6:120;

then (1 / (Sum (mid (f,1,(len f))))) * (Sum (mid ((L (#) F),1,(len (L (#) F))))) = Sum (mid ((L (#) F),1,(len (L (#) F)))) by RLVECT_1:def 8

.= Sum (L (#) F) by A73, A10, FINSEQ_6:120 ;

hence Sum L in M by A3, A4, A6, A86, A10, RLVECT_2:def 8; :: thesis: verum