let X be RealLinearSpace; :: thesis:
let M be Subset of X; :: thesis:
thus ( M is convex implies for n being non zero 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:

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;
assume A1: M is convex ; :: thesis:
A2: for n being non zero Nat st S₁[n] holds
S₁[n + 1]

let n be non zero Nat; :: thesis:
assume A3: 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
A4: len p = n + 1 and
A5: len y = n + 1 and
A6: len z = n + 1 and
A7: Sum p = 1 and
A8: 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));
A9: dom (p | n) = Seg (len (p | n)) by FINSEQ_1:def 3;
1 <= n + 1 by NAT_1:14;
then 1 in Seg (n + 1) by FINSEQ_1:1;
then p . 1 > 0 by A8;
then A10: (p | n) . 1 > 0 by FINSEQ_3:112, NAT_1:14;
p | n = p | (Seg n) by FINSEQ_1:def 16;
then p = (p | n) ^ <*(p . (n + 1))*> by A4, FINSEQ_3:55;
then A11: 1 = (Sum (p | n)) + (p . (n + 1)) by A7, RVSUM_1:74;
A12: 0 + n <= 1 + n by XREAL_1:6;
then A13: len (p | n) = n by A4, FINSEQ_1:59;
then A14: dom (p | n) = Seg n by FINSEQ_1:def 3;
A15: Seg n c= Seg (n + 1) by A12, FINSEQ_1:5;
A16: for i being Nat st i in dom (p | n) holds
0 <= (p | n) . i

proof

let i be Nat; :: thesis:
assume A17: i in dom (p | n) ; :: thesis:
then A18: i <= n by A14, FINSEQ_1:1;
p . i > 0 by A8, A14, A15, A17;
hence 0 <= (p | n) . i by A18, FINSEQ_3:112; :: thesis:

end;

set y9 = y | n;
set p9 = (1 / (1 - (p . (n + 1)))) * (p | n);
deffunc H₁( Nat) -> Element of the carrier of X = (((1 / (1 - (p . (n + 1)))) * (p | n)) . $1) * ((y | n) /. $1);
consider z9 being FinSequence of the carrier of X such that
A19: len z9 = n and
A20: for i being Nat st i in dom z9 holds
z9 . i = H₁(i) from FINSEQ_2:sch 1();
A21: len (y | n) = n by A5, A12, FINSEQ_1:59;
then A22: dom (y | n) = Seg n by FINSEQ_1:def 3;
A23: for i being Nat
for v being VECTOR of X st i in dom z9 & v = (z | n) . i holds
z9 . i = (1 / (1 - (p . (n + 1)))) * v

proof

let i be Nat; :: thesis:
let v be VECTOR of X; :: thesis:
assume that
A24: i in dom z9 and
A25: v = (z | n) . i ; :: thesis:
A26: i in Seg n by A19, A24, FINSEQ_1:def 3;
then A27: (y | n) /. i = y /. i by A22, FINSEQ_4:70;
A28: i <= n by A26, FINSEQ_1:1;
then A29: (z | n) . i = z . i by FINSEQ_3:112;
z9 . i = (((1 / (1 - (p . (n + 1)))) * (p | n)) . i) * ((y | n) /. i) by A20, A24
.= ((1 / (1 - (p . (n + 1)))) * ((p | n) . i)) * ((y | n) /. i) by RVSUM_1:44
.= ((1 / (1 - (p . (n + 1)))) * (p . i)) * ((y | n) /. i) by A28, FINSEQ_3:112
.= (1 / (1 - (p . (n + 1)))) * ((p . i) * ((y | n) /. i)) by RLVECT_1:def 7
.= (1 / (1 - (p . (n + 1)))) * v by A8, A15, A25, A26, A29, A27 ;
hence z9 . i = (1 / (1 - (p . (n + 1)))) * v ; :: thesis:

end;

1 <= n by NAT_1:14;
then 1 in Seg n by FINSEQ_1:1;
then A30: 1 - (p . (n + 1)) > 0 by A11, A14, A16, A10, RVSUM_1:85;
dom ((1 / (1 - (p . (n + 1)))) * (p | n)) = Seg (len ((1 / (1 - (p . (n + 1)))) * (p | n))) by FINSEQ_1:def 3;
then Seg (len ((1 / (1 - (p . (n + 1)))) * (p | n))) = Seg (len (p | n)) by A9, VALUED_1:def 5;
then A31: len ((1 / (1 - (p . (n + 1)))) * (p | n)) = n by A13, FINSEQ_1:6;
A32: n + 1 in Seg (n + 1) by FINSEQ_1:4;
then A33: y /. (n + 1) in M by A8;
A34: 1 - (p . (n + 1)) < 1 by A8, A32, XREAL_1:44;
z | n = z | (Seg n) by FINSEQ_1:def 16;
then A35: z = (z | n) ^ <*(z . (n + 1))*> by A6, FINSEQ_3:55;
z . (n + 1) = (p . (n + 1)) * (y /. (n + 1)) by A8, A32;
then A36: Sum z = (Sum (z | n)) + (Sum <*((p . (n + 1)) * (y /. (n + 1)))*>) by A35, RLVECT_1:41
.= (Sum (z | n)) + ((1 - (1 - (p . (n + 1)))) * (y /. (n + 1))) by RLVECT_1:44 ;
A37: dom z9 = Seg n by A19, FINSEQ_1:def 3;
A38: for i being Nat st i in Seg n holds
( ((1 / (1 - (p . (n + 1)))) * (p | n)) . i > 0 & z9 . i = (((1 / (1 - (p . (n + 1)))) * (p | n)) . i) * ((y | n) /. i) & (y | n) /. i in M )

proof

(1 - (p . (n + 1))) " > 0 by A30;
then A39: 1 / (1 - (p . (n + 1))) > 0 ;
let i be Nat; :: thesis:
assume A40: i in Seg n ; :: thesis:
then A41: i <= n by FINSEQ_1:1;
A42: ((1 / (1 - (p . (n + 1)))) * (p | n)) . i = (1 / (1 - (p . (n + 1)))) * ((p | n) . i) by RVSUM_1:44
.= (1 / (1 - (p . (n + 1)))) * (p . i) by A41, FINSEQ_3:112 ;
AAA: (1 / (1 - (p . (n + 1)))) * (p . i) = (1 / (1 - (p . (n + 1)))) * (p . i) ;
A43: Seg n c= Seg (n + 1) by A12, FINSEQ_1:5;
then p . i > 0 by A8, A40;
hence ((1 / (1 - (p . (n + 1)))) * (p | n)) . i > 0 by A39, A42, AAA; :: thesis:
thus z9 . i = (((1 / (1 - (p . (n + 1)))) * (p | n)) . i) * ((y | n) /. i) by A20, A37, A40; :: thesis:
y /. i in M by A8, A40, A43;
hence (y | n) /. i in M by A22, A40, FINSEQ_4:70; :: thesis:

end;

len (z | n) = n by A6, A12, FINSEQ_1:59;
then A44: (1 - (p . (n + 1))) * (Sum z9) = (1 - (p . (n + 1))) * ((1 / (1 - (p . (n + 1)))) * (Sum (z | n))) by A19, A23, RLVECT_1:39
.= ((1 - (p . (n + 1))) * (1 / (1 - (p . (n + 1))))) * (Sum (z | n)) by RLVECT_1:def 7
.= 1 * (Sum (z | n)) by A30, XCMPLX_1:106
.= Sum (z | n) by RLVECT_1:def 8 ;
Sum ((1 / (1 - (p . (n + 1)))) * (p | n)) = (1 / (1 - (p . (n + 1)))) * (1 - (p . (n + 1))) by A11, RVSUM_1:87
.= 1 by A30, XCMPLX_1:106 ;
then Sum z9 in M by A3, A19, A31, A21, A38;
hence Sum z in M by A1, A33, A34, A30, A36, A44, CONVEX1:def 2; :: thesis:

end;

A45: S₁[1]

proof

let p be FinSequence of REAL ; :: thesis:
let y, z be FinSequence of the carrier of X; :: thesis:
assume that
A46: len p = 1 and
len y = 1 and
A47: len z = 1 and
A48: Sum p = 1 and
A49: for i being Nat st i in Seg 1 holds
( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) ; :: thesis:
reconsider p1 = p . 1 as Element of REAL by XREAL_0:def 1;
p = <*p1*> by A46, FINSEQ_1:40;
then A50: p . 1 = 1 by A48, FINSOP_1:11;
A51: 1 in Seg 1 by FINSEQ_1:2, TARSKI:def 1;
then z . 1 = (p . 1) * (y /. 1) by A49;
then A52: z . 1 = y /. 1 by A50, RLVECT_1:def 8;
A53: z = <*(z . 1)*> by A47, FINSEQ_1:40;
y /. 1 in M by A49, A51;
hence Sum z in M by A53, A52, RLVECT_1:44; :: thesis:

end;

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

end;

thus ( ( for n being non zero 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 A54: for n being non zero 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
A55: 0 < r and
A56: r < 1 and
A57: x1 in M and
A58: x2 in M ; :: thesis:
set z = <*(r * x1),((1 - r) * x2)*>;
set y = <*x1,x2*>;
reconsider r = r as Element of REAL by XREAL_0:def 1;
reconsider r1 = 1 - r as Element of REAL by XREAL_0:def 1;
set p = <*r,r1*>;
A59: for i being Nat st i in Seg 2 holds
( <*r,r1*> . i > 0 & <*(r * x1),((1 - r) * x2)*> . i = (<*r,r1*> . i) * (<*x1,x2*> /. i) & <*x1,x2*> /. i in M )

proof

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

per cases by A60, FINSEQ_1:2, TARSKI:def 2;

suppose A61: i = 1 ; :: thesis:

then A62: <*x1,x2*> /. i = x1 by FINSEQ_4:17;
thus ( <*r,r1*> . i > 0 & <*(r * x1),((1 - r) * x2)*> . i = (<*r,r1*> . i) * (<*x1,x2*> /. i) & <*x1,x2*> /. i in M ) by A55, A57, A61, A62; :: thesis:

end;

suppose A63: i = 2 ; :: thesis:

then A64: <*x1,x2*> /. i = x2 by FINSEQ_4:17;
thus ( <*r,r1*> . i > 0 & <*(r * x1),((1 - r) * x2)*> . i = (<*r,r1*> . i) * (<*x1,x2*> /. i) & <*x1,x2*> /. i in M ) by A56, A58, A63, A64, XREAL_1:50; :: thesis:

end;

A65: len <*x1,x2*> = 2 by FINSEQ_1:44;
A66: Sum <*r,r1*> = r + (1 - r) by RVSUM_1:77
.= 1 ;
A67: len <*(r * x1),((1 - r) * x2)*> = 2 by FINSEQ_1:44;
len <*r,r1*> = 2 by FINSEQ_1:44;
then Sum <*(r * x1),((1 - r) * x2)*> in M by A54, A65, A67, A66, A59;
hence (r * x1) + ((1 - r) * x2) in M by RLVECT_1:45; :: thesis:

end;

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

end;