let V be non empty RealUnitarySpace-like UNITSTR ; :: thesis: for M being Subset of V
for F being FinSequence of the carrier of V
for B being FinSequence of REAL st M = { u where u is VECTOR of V : for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & u .|. v <= B . i )
}
holds
M is convex

let M be Subset of V; :: thesis: for F being FinSequence of the carrier of V
for B being FinSequence of REAL st M = { u where u is VECTOR of V : for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & u .|. v <= B . i )
}
holds
M is convex

let F be FinSequence of the carrier of V; :: thesis: for B being FinSequence of REAL st M = { u where u is VECTOR of V : for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & u .|. v <= B . i )
}
holds
M is convex

let B be FinSequence of REAL ; :: thesis: ( M = { u where u is VECTOR of V : for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & u .|. v <= B . i )
}
implies M is convex )

assume A1: M = { u where u is VECTOR of V : for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & u .|. v <= B . i )
}
; :: thesis: M is convex
let u1, v1 be VECTOR of V; :: according to CONVEX1:def 2 :: thesis: for b1 being object holds
( b1 <= 0 or 1 <= b1 or not u1 in M or not v1 in M or (b1 * u1) + ((1 - b1) * v1) in M )

let r be Real; :: thesis: ( r <= 0 or 1 <= r or not u1 in M or not v1 in M or (r * u1) + ((1 - r) * v1) in M )
assume that
A2: 0 < r and
A3: r < 1 and
A4: u1 in M and
A5: v1 in M ; :: thesis: (r * u1) + ((1 - r) * v1) in M
consider v9 being VECTOR of V such that
A6: v1 = v9 and
A7: for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & v9 .|. v <= B . i ) by A1, A5;
consider u9 being VECTOR of V such that
A8: u1 = u9 and
A9: for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & u9 .|. v <= B . i ) by A1, A4;
for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & ((r * u1) + ((1 - r) * v1)) .|. v <= B . i )
proof
0 + r < 1 by A3;
then A10: 1 - r > 0 by XREAL_1:20;
let i be Element of NAT ; :: thesis: ( i in (dom F) /\ (dom B) implies ex v being VECTOR of V st
( v = F . i & ((r * u1) + ((1 - r) * v1)) .|. v <= B . i ) )

assume A11: i in (dom F) /\ (dom B) ; :: thesis: ex v being VECTOR of V st
( v = F . i & ((r * u1) + ((1 - r) * v1)) .|. v <= B . i )

reconsider b = B . i as Real ;
consider x being VECTOR of V such that
A12: x = F . i and
A13: u9 .|. x <= b by ;
take v = x; :: thesis: ( v = F . i & ((r * u1) + ((1 - r) * v1)) .|. v <= B . i )
A14: ((r * u1) + ((1 - r) * v1)) .|. v = ((r * u1) .|. v) + (((1 - r) * v1) .|. v) by BHSP_1:def 2
.= (r * (u1 .|. v)) + (((1 - r) * v1) .|. v) by BHSP_1:def 2
.= (r * (u1 .|. v)) + ((1 - r) * (v1 .|. v)) by BHSP_1:def 2 ;
r * (u1 .|. v) <= r * b by ;
then ((r * u1) + ((1 - r) * v1)) .|. v <= (r * b) + ((1 - r) * (v1 .|. v)) by ;
then A15: (((r * u1) + ((1 - r) * v1)) .|. v) - (r * b) <= (1 - r) * (v1 .|. v) by XREAL_1:20;
ex y being VECTOR of V st
( y = F . i & v9 .|. y <= b ) by ;
then (1 - r) * (v1 .|. v) <= (1 - r) * b by ;
then (((r * u1) + ((1 - r) * v1)) .|. v) - (r * b) <= (1 - r) * b by ;
then ((r * u1) + ((1 - r) * v1)) .|. v <= (r * b) + ((1 - r) * b) by XREAL_1:20;
hence ( v = F . i & ((r * u1) + ((1 - r) * v1)) .|. v <= B . i ) by A12; :: thesis: verum
end;
hence (r * u1) + ((1 - r) * v1) in M by A1; :: thesis: verum