let X be RealLinearSpace; :: thesis:
let M be Subset of X; :: thesis:
thus ( M is convex implies for n being non empty Nat
for p being FinSequence of REAL
for y, z being FinSequence of the carrier of X st len p = n & len y = n & len z = n & Sum p = 1 & ( for i being Nat st i in Seg n holds
( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) ) holds
Sum z in M ) :: thesis:

proof

assume A1: M is convex ; :: thesis:
defpred S₁[ Nat] means for p being FinSequence of REAL
for y, z being FinSequence of the carrier of X st len p = $1 & len y = $1 & len z = $1 & Sum p = 1 & ( for i being Nat st i in Seg $1 holds
( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) ) holds
Sum z in M;
A2: S₁[1]

proof

let p be FinSequence of REAL ; :: thesis:
let y, z be FinSequence of the carrier of X; :: thesis:
assume that
A3: ( len p = 1 & len y = 1 & len z = 1 ) and
A4: Sum p = 1 and
A5: for i being Nat st i in Seg 1 holds
( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) ; :: thesis:
A6: ( p = <*(p . 1)*> & z = <*(z . 1)*> ) by A3, FINSEQ_1:57;
1 in Seg 1 by FINSEQ_1:4, TARSKI:def 1;
then A7: ( z . 1 = (p . 1) * (y /. 1) & y /. 1 in M ) by A5;
p . 1 = 1 by A4, A6, FINSOP_1:12;
then z . 1 = y /. 1 by A7, RLVECT_1:def 9;
hence Sum z in M by A6, A7, RLVECT_1:61; :: thesis:

end;

A8: for n being non empty Nat st S₁[n] holds
S₁[n + 1]

proof

let n be non empty Nat; :: thesis:
assume A9: S₁[n] ; :: thesis:
thus for p being FinSequence of REAL
for y, z being FinSequence of the carrier of X st len p = n + 1 & len y = n + 1 & len z = n + 1 & Sum p = 1 & ( for i being Nat st i in Seg (n + 1) holds
( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) ) holds
Sum z in M :: thesis:

proof

let p be FinSequence of REAL ; :: thesis:
let y, z be FinSequence of the carrier of X; :: thesis:
assume that
A10: ( len p = n + 1 & len y = n + 1 & len z = n + 1 ) and
A11: Sum p = 1 and
A12: for i being Nat st i in Seg (n + 1) holds
( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) ; :: thesis:
set q = 1 - (p . (n + 1));
n + 1 in Seg (n + 1) by FINSEQ_1:6;
then A13: ( p . (n + 1) > 0 & z . (n + 1) = (p . (n + 1)) * (y /. (n + 1)) & y /. (n + 1) in M ) by A12;
then A14: 1 - (p . (n + 1)) < 1 by XREAL_1:46;
( len p = n + 1 & p | n = p | (Seg n) ) by A10, FINSEQ_1:def 15;
then p = (p | n) ^ <*(p . (n + 1))*> by FINSEQ_3:61;
then A15: 1 = (Sum (p | n)) + (p . (n + 1)) by A11, RVSUM_1:104;
A16: 0 + n <= 1 + n by XREAL_1:8;
then A17: len (p | n) = n by A10, FINSEQ_1:80;
then A18: dom (p | n) = Seg n by FINSEQ_1:def 3;
A19: Seg n c= Seg (n + 1) by A16, FINSEQ_1:7;
A20: for i being Nat st i in dom (p | n) holds
0 <= (p | n) . i

proof

let i be Nat; :: thesis:
assume A21: i in dom (p | n) ; :: thesis:
then A22: i <= n by A18, FINSEQ_1:3;
p . i > 0 by A12, A18, A19, A21;
hence 0 <= (p | n) . i by A22, FINSEQ_3:121; :: thesis:

end;

( 1 <= n & 1 <= n + 1 ) by NAT_1:14;
then A23: ( 1 in Seg n & 1 in Seg (n + 1) ) by FINSEQ_1:3;
then p . 1 > 0 by A12;
then (p | n) . 1 > 0 by FINSEQ_3:121, NAT_1:14;
then A24: 1 - (p . (n + 1)) > 0 by A15, A18, A20, A23, RVSUM_1:115;
set p' = (1 / (1 - (p . (n + 1)))) * (p | n);
set y' = y | n;
deffunc H₁( Nat) -> Element of the carrier of X = (((1 / (1 - (p . (n + 1)))) * (p | n)) . $1) * ((y | n) /. $1);
consider z' being FinSequence of the carrier of X such that
A25: len z' = n and
A26: for i being Nat st i in dom z' holds
z' . i = H₁(i) from FINSEQ_2:sch 1();
A27: dom z' = Seg n by A25, FINSEQ_1:def 3;
( dom ((1 / (1 - (p . (n + 1)))) * (p | n)) = Seg (len ((1 / (1 - (p . (n + 1)))) * (p | n))) & dom (p | n) = Seg (len (p | n)) ) by FINSEQ_1:def 3;
then Seg (len ((1 / (1 - (p . (n + 1)))) * (p | n))) = Seg (len (p | n)) by VALUED_1:def 5;
then A28: len ((1 / (1 - (p . (n + 1)))) * (p | n)) = n by A17, FINSEQ_1:8;
A29: len (y | n) = n by A10, A16, FINSEQ_1:80;
then A30: dom (y | n) = Seg n by FINSEQ_1:def 3;
A31: Sum ((1 / (1 - (p . (n + 1)))) * (p | n)) = (1 / (1 - (p . (n + 1)))) * (1 - (p . (n + 1))) by A15, RVSUM_1:117
.= 1 by A24, XCMPLX_1:107 ;
for i being Nat st i in Seg n holds
( ((1 / (1 - (p . (n + 1)))) * (p | n)) . i > 0 & z' . i = (((1 / (1 - (p . (n + 1)))) * (p | n)) . i) * ((y | n) /. i) & (y | n) /. i in M )

proof

let i be Nat; :: thesis:
assume A32: i in Seg n ; :: thesis:
then A33: i <= n by FINSEQ_1:3;
Seg n c= Seg (n + 1) by A16, FINSEQ_1:7;
then A34: ( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) by A12, A32;
(1 - (p . (n + 1))) " > 0 by A24;
then A35: 1 / (1 - (p . (n + 1))) > 0 by XCMPLX_1:217;
((1 / (1 - (p . (n + 1)))) * (p | n)) . i = (1 / (1 - (p . (n + 1)))) * ((p | n) . i) by RVSUM_1:66
.= (1 / (1 - (p . (n + 1)))) * (p . i) by A33, FINSEQ_3:121 ;
hence ((1 / (1 - (p . (n + 1)))) * (p | n)) . i > 0 by A34, A35, XREAL_1:131; :: thesis:
thus z' . i = (((1 / (1 - (p . (n + 1)))) * (p | n)) . i) * ((y | n) /. i) by A26, A32, A27; :: thesis:
thus (y | n) /. i in M by A30, A32, A34, FINSEQ_4:85; :: thesis:

end;

then A36: Sum z' in M by A9, A25, A28, A29, A31;
( len z = n + 1 & z | n = z | (Seg n) ) by A10, FINSEQ_1:def 15;
then z = (z | n) ^ <*(z . (n + 1))*> by FINSEQ_3:61;
then A37: Sum z = (Sum (z | n)) + (Sum <*((p . (n + 1)) * (y /. (n + 1)))*>) by A13, RLVECT_1:58
.= (Sum (z | n)) + ((1 - (1 - (p . (n + 1)))) * (y /. (n + 1))) by RLVECT_1:61 ;
A38: len (z | n) = n by A10, A16, FINSEQ_1:80;
for i being Element of NAT
for v being VECTOR of X st i in dom z' & v = (z | n) . i holds
z' . i = (1 / (1 - (p . (n + 1)))) * v

proof

let i be Element of NAT ; :: thesis:
let v be VECTOR of X; :: thesis:
assume that
A39: i in dom z' and
A40: v = (z | n) . i ; :: thesis:
A41: i in Seg n by A25, A39, FINSEQ_1:def 3;
then A42: i <= n by FINSEQ_1:3;
then A43: (z | n) . i = z . i by FINSEQ_3:121;
A44: (y | n) /. i = y /. i by A30, A41, FINSEQ_4:85;
z' . i = (((1 / (1 - (p . (n + 1)))) * (p | n)) . i) * ((y | n) /. i) by A26, A41, A27
.= ((1 / (1 - (p . (n + 1)))) * ((p | n) . i)) * ((y | n) /. i) by RVSUM_1:66
.= ((1 / (1 - (p . (n + 1)))) * (p . i)) * ((y | n) /. i) by A42, FINSEQ_3:121
.= (1 / (1 - (p . (n + 1)))) * ((p . i) * ((y | n) /. i)) by RLVECT_1:def 9
.= (1 / (1 - (p . (n + 1)))) * v by A12, A19, A40, A41, A43, A44 ;
hence z' . i = (1 / (1 - (p . (n + 1)))) * v ; :: thesis:

end;

then (1 - (p . (n + 1))) * (Sum z') = (1 - (p . (n + 1))) * ((1 / (1 - (p . (n + 1)))) * (Sum (z | n))) by A25, A38, RLVECT_1:56
.= ((1 - (p . (n + 1))) * (1 / (1 - (p . (n + 1))))) * (Sum (z | n)) by RLVECT_1:def 9
.= 1 * (Sum (z | n)) by A24, XCMPLX_1:107
.= Sum (z | n) by RLVECT_1:def 9 ;
hence Sum z in M by A1, A13, A14, A24, A36, A37, CONVEX1:def 2; :: thesis:

end;

thus for n being non empty Nat holds S₁[n] from NAT_1:sch 10(A2, A8); :: thesis:

end;

thus ( ( for n being non empty Nat
for p being FinSequence of REAL
for y, z being FinSequence of the carrier of X st len p = n & len y = n & len z = n & Sum p = 1 & ( for i being Nat st i in Seg n holds
( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) ) holds
Sum z in M ) implies M is convex ) :: thesis:

proof

assume A45: for n being non empty Nat
for p being FinSequence of REAL
for y, z being FinSequence of the carrier of X st len p = n & len y = n & len z = n & Sum p = 1 & ( for i being Nat st i in Seg n holds
( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) ) holds
Sum z in M ; :: thesis:
for x1, x2 being VECTOR of X
for r being Real st 0 < r & r < 1 & x1 in M & x2 in M holds
(r * x1) + ((1 - r) * x2) in M

proof

let x1, x2 be VECTOR of X; :: thesis:
let r be Real; :: thesis:
assume that
A46: ( 0 < r & r < 1 ) and
A47: ( x1 in M & x2 in M ) ; :: thesis:
set p = <*r,(1 - r)*>;
set y = <*x1,x2*>;
set z = <*(r * x1),((1 - r) * x2)*>;
A48: ( len <*r,(1 - r)*> = 2 & len <*x1,x2*> = 2 & len <*(r * x1),((1 - r) * x2)*> = 2 ) by FINSEQ_1:61;
A49: Sum <*r,(1 - r)*> = r + (1 - r) by RVSUM_1:107
.= 1 ;
for i being Nat st i in Seg 2 holds
( <*r,(1 - r)*> . i > 0 & <*(r * x1),((1 - r) * x2)*> . i = (<*r,(1 - r)*> . i) * (<*x1,x2*> /. i) & <*x1,x2*> /. i in M )

proof

let i be Nat; :: thesis:
assume A50: i in Seg 2 ; :: thesis:

per cases by A50, FINSEQ_1:4, TARSKI:def 2;

suppose i = 1 ; :: thesis:

then ( <*r,(1 - r)*> . i = r & <*x1,x2*> /. i = x1 & <*(r * x1),((1 - r) * x2)*> . i = r * x1 ) by FINSEQ_1:61, FINSEQ_4:26;
hence ( <*r,(1 - r)*> . i > 0 & <*(r * x1),((1 - r) * x2)*> . i = (<*r,(1 - r)*> . i) * (<*x1,x2*> /. i) & <*x1,x2*> /. i in M ) by A46, A47; :: thesis:

end;

suppose i = 2 ; :: thesis:

then ( <*r,(1 - r)*> . i = 1 - r & <*x1,x2*> /. i = x2 & <*(r * x1),((1 - r) * x2)*> . i = (1 - r) * x2 ) by FINSEQ_1:61, FINSEQ_4:26;
hence ( <*r,(1 - r)*> . i > 0 & <*(r * x1),((1 - r) * x2)*> . i = (<*r,(1 - r)*> . i) * (<*x1,x2*> /. i) & <*x1,x2*> /. i in M ) by A46, A47, XREAL_1:52; :: thesis:

end;

then Sum <*(r * x1),((1 - r) * x2)*> in M by A45, A48, A49;
hence (r * x1) + ((1 - r) * x2) in M by RLVECT_1:62; :: thesis:

end;

hence M is convex by CONVEX1:def 2; :: thesis:

end;