let X be RealLinearSpace; :: thesis: for M being Subset of X holds

( M is convex iff 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 )

let M be Subset of X; :: thesis: ( M is convex iff 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 )

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

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

( M is convex iff 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 )

let M be Subset of X; :: thesis: ( M is convex iff 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 )

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

proof

thus
( ( for n being non zero Nat
defpred S_{1}[ 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: 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

A2: for n being non zero Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[1]
_{1}[n]
from NAT_1:sch 10(A45, A2); :: thesis: verum

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

A2: for n being non zero Nat st S

S

proof

A45:
S
let n be non zero Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A3: S_{1}[n]
; :: thesis: S_{1}[n + 1]

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

end;assume A3: S

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

proof

let p be FinSequence of REAL ; :: thesis: 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

let y, z be FinSequence of the carrier of X; :: thesis: ( 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 ) ) implies Sum z in M )

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: Sum z in M

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 15;

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

set p9 = (1 / (1 - (p . (n + 1)))) * (p | n);

deffunc H_{1}( 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_{1}(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

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 15;

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 )

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

end;( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) ) holds

Sum z in M

let y, z be FinSequence of the carrier of X; :: thesis: ( 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 ) ) implies Sum z in M )

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: Sum z in M

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 15;

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

set y9 = y | n;
let i be Nat; :: thesis: ( i in dom (p | n) implies 0 <= (p | n) . i )

assume A17: i in dom (p | n) ; :: thesis: 0 <= (p | n) . i

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

end;assume A17: i in dom (p | n) ; :: thesis: 0 <= (p | n) . i

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

set p9 = (1 / (1 - (p . (n + 1)))) * (p | n);

deffunc H

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

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

1 <= n
by NAT_1:14;
let i be Nat; :: thesis: for v being VECTOR of X st i in dom z9 & v = (z | n) . i holds

z9 . i = (1 / (1 - (p . (n + 1)))) * v

let v be VECTOR of X; :: thesis: ( i in dom z9 & v = (z | n) . i implies z9 . i = (1 / (1 - (p . (n + 1)))) * v )

assume that

A24: i in dom z9 and

A25: v = (z | n) . i ; :: thesis: z9 . i = (1 / (1 - (p . (n + 1)))) * v

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

end;z9 . i = (1 / (1 - (p . (n + 1)))) * v

let v be VECTOR of X; :: thesis: ( i in dom z9 & v = (z | n) . i implies z9 . i = (1 / (1 - (p . (n + 1)))) * v )

assume that

A24: i in dom z9 and

A25: v = (z | n) . i ; :: thesis: z9 . i = (1 / (1 - (p . (n + 1)))) * v

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

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 15;

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

len (z | n) = n
by A6, A12, FINSEQ_1:59;
(1 - (p . (n + 1))) " > 0
by A30;

then A39: 1 / (1 - (p . (n + 1))) > 0 by XCMPLX_1:215;

let i be Nat; :: thesis: ( i in Seg n implies ( ((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 ) )

assume A40: i in Seg n ; :: thesis: ( ((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 )

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 ;

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; :: thesis: ( z9 . i = (((1 / (1 - (p . (n + 1)))) * (p | n)) . i) * ((y | n) /. i) & (y | n) /. i in M )

thus z9 . i = (((1 / (1 - (p . (n + 1)))) * (p | n)) . i) * ((y | n) /. i) by A20, A37, A40; :: thesis: (y | n) /. i in M

y /. i in M by A8, A40, A43;

hence (y | n) /. i in M by A22, A40, FINSEQ_4:70; :: thesis: verum

end;then A39: 1 / (1 - (p . (n + 1))) > 0 by XCMPLX_1:215;

let i be Nat; :: thesis: ( i in Seg n implies ( ((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 ) )

assume A40: i in Seg n ; :: thesis: ( ((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 )

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 ;

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; :: thesis: ( z9 . i = (((1 / (1 - (p . (n + 1)))) * (p | n)) . i) * ((y | n) /. i) & (y | n) /. i in M )

thus z9 . i = (((1 / (1 - (p . (n + 1)))) * (p | n)) . i) * ((y | n) /. i) by A20, A37, A40; :: thesis: (y | n) /. i in M

y /. i in M by A8, A40, A43;

hence (y | n) /. i in M by A22, A40, FINSEQ_4:70; :: thesis: verum

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

proof

thus
for n being non zero Nat holds S
let p be FinSequence of REAL ; :: thesis: 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

let y, z be FinSequence of the carrier of X; :: thesis: ( 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 ) ) implies Sum z in M )

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: Sum z in M

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

end;( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) ) holds

Sum z in M

let y, z be FinSequence of the carrier of X; :: thesis: ( 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 ) ) implies Sum z in M )

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: Sum z in M

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

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

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: M is convex

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

end;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: M is convex

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

hence
M is convex
by CONVEX1:def 2; :: thesis: verum
let x1, x2 be VECTOR of X; :: thesis: for r being Real st 0 < r & r < 1 & x1 in M & x2 in M holds

(r * x1) + ((1 - r) * x2) in M

let r be Real; :: thesis: ( 0 < r & r < 1 & x1 in M & x2 in M implies (r * x1) + ((1 - r) * x2) in M )

assume that

A55: 0 < r and

A56: r < 1 and

A57: x1 in M and

A58: x2 in M ; :: thesis: (r * x1) + ((1 - r) * x2) in M

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 )

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

end;(r * x1) + ((1 - r) * x2) in M

let r be Real; :: thesis: ( 0 < r & r < 1 & x1 in M & x2 in M implies (r * x1) + ((1 - r) * x2) in M )

assume that

A55: 0 < r and

A56: r < 1 and

A57: x1 in M and

A58: x2 in M ; :: thesis: (r * x1) + ((1 - r) * x2) in M

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

A65:
len <*x1,x2*> = 2
by FINSEQ_1:44;
let i be Nat; :: thesis: ( i in Seg 2 implies ( <*r,r1*> . i > 0 & <*(r * x1),((1 - r) * x2)*> . i = (<*r,r1*> . i) * (<*x1,x2*> /. i) & <*x1,x2*> /. i in M ) )

assume A60: i in Seg 2 ; :: thesis: ( <*r,r1*> . i > 0 & <*(r * x1),((1 - r) * x2)*> . i = (<*r,r1*> . i) * (<*x1,x2*> /. i) & <*x1,x2*> /. i in M )

end;assume A60: i in Seg 2 ; :: thesis: ( <*r,r1*> . i > 0 & <*(r * x1),((1 - r) * x2)*> . i = (<*r,r1*> . i) * (<*x1,x2*> /. i) & <*x1,x2*> /. i in M )

per cases
( i = 1 or i = 2 )
by A60, FINSEQ_1:2, TARSKI:def 2;

end;

suppose A61:
i = 1
; :: thesis: ( <*r,r1*> . i > 0 & <*(r * x1),((1 - r) * x2)*> . i = (<*r,r1*> . i) * (<*x1,x2*> /. i) & <*x1,x2*> /. i in M )

then A62:
<*x1,x2*> /. i = x1
by FINSEQ_4:17;

<*r,r1*> . i = r by A61, FINSEQ_1:44;

hence ( <*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, FINSEQ_1:44; :: thesis: verum

end;<*r,r1*> . i = r by A61, FINSEQ_1:44;

hence ( <*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, FINSEQ_1:44; :: thesis: verum

suppose A63:
i = 2
; :: thesis: ( <*r,r1*> . i > 0 & <*(r * x1),((1 - r) * x2)*> . i = (<*r,r1*> . i) * (<*x1,x2*> /. i) & <*x1,x2*> /. i in M )

then A64:
<*x1,x2*> /. i = x2
by FINSEQ_4:17;

<*r,r1*> . i = 1 - r by A63, FINSEQ_1:44;

hence ( <*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, FINSEQ_1:44, XREAL_1:50; :: thesis: verum

end;<*r,r1*> . i = 1 - r by A63, FINSEQ_1:44;

hence ( <*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, FINSEQ_1:44, XREAL_1:50; :: thesis: verum

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