:: CONVEX2 semantic presentation begin reconsider rr = 1 as Real ; set ff = <*rr*>; theorem :: CONVEX2:1 for V being non empty RLSStruct for M, N being convex Subset of V holds M /\ N is convex ; theorem :: CONVEX2:2 for V being non empty RealUnitarySpace-like UNITSTR 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 proof 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 Element of REAL 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 ) then i in dom B by XBOOLE_0:def_4; then reconsider b = B . i as Real by PARTFUN1:4; consider x being VECTOR of V such that A12: x = F . i and A13: u9 .|. x <= b by A9, A11; 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 A2, A8, A13, XREAL_1:64; then ((r * u1) + ((1 - r) * v1)) .|. v <= (r * b) + ((1 - r) * (v1 .|. v)) by A14, XREAL_1:6; 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 A7, A11; then (1 - r) * (v1 .|. v) <= (1 - r) * b by A6, A12, A10, XREAL_1:64; then (((r * u1) + ((1 - r) * v1)) .|. v) - (r * b) <= (1 - r) * b by A15, XXREAL_0:2; 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 end; theorem :: CONVEX2:3 for V being non empty RealUnitarySpace-like UNITSTR 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 proof 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 Element of REAL 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 ) then i in dom B by XBOOLE_0:def_4; then reconsider b = B . i as Real by PARTFUN1:4; consider x being VECTOR of V such that A12: x = F . i and A13: u9 .|. x < b by A9, A11; 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 A2, A8, A13, XREAL_1:68; then ((r * u1) + ((1 - r) * v1)) .|. v < (r * b) + ((1 - r) * (v1 .|. v)) by A14, XREAL_1:8; then A15: (((r * u1) + ((1 - r) * v1)) .|. v) - (r * b) < (1 - r) * (v1 .|. v) by XREAL_1:19; ex y being VECTOR of V st ( y = F . i & v9 .|. y < b ) by A7, A11; then (1 - r) * (v1 .|. v) <= (1 - r) * b by A6, A12, A10, XREAL_1:64; then (((r * u1) + ((1 - r) * v1)) .|. v) - (r * b) < (1 - r) * b by A15, XXREAL_0:2; then ((r * u1) + ((1 - r) * v1)) .|. v < (r * b) + ((1 - r) * b) by XREAL_1:19; 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 end; theorem :: CONVEX2:4 for V being non empty RealUnitarySpace-like UNITSTR 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 proof 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 Element of REAL 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 ) then i in dom B by XBOOLE_0:def_4; then reconsider b = B . i as Real by PARTFUN1:4; consider x being VECTOR of V such that A12: x = F . i and A13: u9 .|. x >= b by A9, A11; 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 A2, A8, A13, XREAL_1:64; then ((r * u1) + ((1 - r) * v1)) .|. v >= (r * b) + ((1 - r) * (v1 .|. v)) by A14, XREAL_1:6; then A15: (((r * u1) + ((1 - r) * v1)) .|. v) - (r * b) >= (1 - r) * (v1 .|. v) by XREAL_1:19; ex y being VECTOR of V st ( y = F . i & v9 .|. y >= b ) by A7, A11; then (1 - r) * (v1 .|. v) >= (1 - r) * b by A6, A12, A10, XREAL_1:64; then (((r * u1) + ((1 - r) * v1)) .|. v) - (r * b) >= (1 - r) * b by A15, XXREAL_0:2; then ((r * u1) + ((1 - r) * v1)) .|. v >= (r * b) + ((1 - r) * b) by XREAL_1:19; 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 end; theorem :: CONVEX2:5 for V being non empty RealUnitarySpace-like UNITSTR 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 proof 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 Element of REAL 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 ) then i in dom B by XBOOLE_0:def_4; then reconsider b = B . i as Real by PARTFUN1:4; consider x being VECTOR of V such that A12: x = F . i and A13: u9 .|. x > b by A9, A11; 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 A2, A8, A13, XREAL_1:68; then ((r * u1) + ((1 - r) * v1)) .|. v > (r * b) + ((1 - r) * (v1 .|. v)) by A14, XREAL_1:8; 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 A7, A11; then (1 - r) * (v1 .|. v) >= (1 - r) * b by A6, A12, A10, XREAL_1:64; then (((r * u1) + ((1 - r) * v1)) .|. v) - (r * b) > (1 - r) * b by A15, XXREAL_0:2; 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 end; Lm1: for V being RealLinearSpace 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 proof 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, CONVEX1:def_3; 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 empty Element of NAT by A3, A4, FINSEQ_4:62; A10: len (L (#) F) = len F by RLVECT_2:def_7; defpred S1[ 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 empty Nat st S1[k] holds S1[k + 1] proof let k be non empty Nat; ::_thesis: ( S1[k] implies S1[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: S1[k + 1] now__::_thesis:_S1[k_+_1] percases ( k >= len f or k < len f ) ; supposeA15: k >= len f ; ::_thesis: S1[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 S1[k + 1] by A14, A17, A18, A16; ::_thesis: verum end; supposeA19: k < len f ; ::_thesis: S1[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 ) proof 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; A25: for i being Nat st i in dom <*((mid (f,1,(k + 1))) . (k + 1))*> holds (mid (f,1,(k + 1))) . ((len (mid (f,1,k))) + i) = <*((mid (f,1,(k + 1))) . (k + 1))*> . i proof 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; A26: mid (f,1,(k + 1)) = f | (k + 1) by FINSEQ_6:116, NAT_1:14; 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 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; then A31: Sum (mid (f,1,k)) > 0 by A21, RVSUM_1:85; 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 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; A41: k + 1 >= 1 by NAT_1:14; 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 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, TARSKI:def_3; ::_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 (Sum (mid (f,1,k))) + (L . (F /. (k + 1))) > Sum (mid (f,1,k)) by XREAL_1:29; 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, XREAL_1:8; 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 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; k + 1 in Seg (k + 1) by A41; 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 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; ( 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; 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 S1[k + 1] by A14, A50, A56, A54, A72, CONVEX1:def_2; ::_thesis: verum end; end; end; hence S1[k + 1] ; ::_thesis: verum end; len F > 0 by A3, A4, A9, CARD_1:27, FINSEQ_4:62; then A73: len F >= 0 + 1 by NAT_1:13; A74: S1[1] proof 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, XBOOLE_1:1; 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 S1[1] by A4, A81, A83, A77; ::_thesis: verum end; for k being non empty Nat holds S1[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 end; Lm2: for V being RealLinearSpace for M being Subset of V st ( 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 ) holds M is convex proof let V be RealLinearSpace; ::_thesis: for M being Subset of V st ( 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 ) holds M is convex let M be 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 ) implies M is convex ) assume A1: 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 ; ::_thesis: M is convex let u, v be VECTOR of V; :: according to CONVEX1:def_2 ::_thesis: for b1 being Element of REAL holds ( b1 <= 0 or 1 <= b1 or not u in M or not v in M or (b1 * u) + ((1 - b1) * v) in M ) let r be Real; ::_thesis: ( r <= 0 or 1 <= r or not u in M or not v in M or (r * u) + ((1 - r) * v) in M ) assume that A2: 0 < r and A3: r < 1 and A4: ( u in M & v in M ) ; ::_thesis: (r * u) + ((1 - r) * v) in M set N = {u,v}; A5: {u,v} c= M by A4, ZFMISC_1:32; reconsider N = {u,v} as Subset of V ; now__::_thesis:_(r_*_u)_+_((1_-_r)_*_v)_in_M percases ( u <> v or u = v ) ; supposeA6: u <> v ; ::_thesis: (r * u) + ((1 - r) * v) in M consider L being Linear_Combination of {u,v} such that A7: ( L . u = r & L . v = 1 - r ) by A6, RLVECT_4:38; reconsider L = L as Linear_Combination of N ; A8: L is convex proof A9: r - r < 1 - r by A3, XREAL_1:9; then v in { w where w is Element of V : L . w <> 0 } by A7; then A10: v in Carrier L by RLVECT_2:def_4; A11: for n being Element of NAT st n in dom <*r,(1 - r)*> holds ( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 ) proof let n be Element of NAT ; ::_thesis: ( n in dom <*r,(1 - r)*> implies ( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 ) ) assume n in dom <*r,(1 - r)*> ; ::_thesis: ( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 ) then n in Seg (len <*r,(1 - r)*>) by FINSEQ_1:def_3; then A12: n in {1,2} by FINSEQ_1:2, FINSEQ_1:44; now__::_thesis:_(_<*r,(1_-_r)*>_._n_=_L_._(<*u,v*>_._n)_&_<*r,(1_-_r)*>_._n_>=_0_) percases ( n = 1 or n = 2 ) by A12, TARSKI:def_2; supposeA13: n = 1 ; ::_thesis: ( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 ) then L . (<*u,v*> . n) = r by A7, FINSEQ_1:44; hence ( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 ) by A2, A13, FINSEQ_1:44; ::_thesis: verum end; supposeA14: n = 2 ; ::_thesis: ( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 ) then L . (<*u,v*> . n) = 1 - r by A7, FINSEQ_1:44; hence ( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 ) by A9, A14, FINSEQ_1:44; ::_thesis: verum end; end; end; hence ( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 ) ; ::_thesis: verum end; u in { w where w is Element of V : L . w <> 0 } by A2, A7; then u in Carrier L by RLVECT_2:def_4; then A15: ( Carrier L c= {u,v} & {u,v} c= Carrier L ) by A10, RLVECT_2:def_6, ZFMISC_1:32; take F = <*u,v*>; :: according to CONVEX1:def_3 ::_thesis: ( F is one-to-one & rng F = Carrier L & ex b1 being FinSequence of REAL st ( len b1 = len F & Sum b1 = 1 & ( for b2 being set holds ( not b2 in dom b1 or ( b1 . b2 = L . (F . b2) & 0 <= b1 . b2 ) ) ) ) ) A16: Sum <*r,(1 - r)*> = r + (1 - r) by RVSUM_1:77 .= 1 ; thus F is one-to-one by A6, FINSEQ_3:94; ::_thesis: ( rng F = Carrier L & ex b1 being FinSequence of REAL st ( len b1 = len F & Sum b1 = 1 & ( for b2 being set holds ( not b2 in dom b1 or ( b1 . b2 = L . (F . b2) & 0 <= b1 . b2 ) ) ) ) ) thus rng F = (rng <*u*>) \/ (rng <*v*>) by FINSEQ_1:31 .= {u} \/ (rng <*v*>) by FINSEQ_1:38 .= {u} \/ {v} by FINSEQ_1:38 .= {u,v} by ENUMSET1:1 .= Carrier L by A15, XBOOLE_0:def_10 ; ::_thesis: ex b1 being FinSequence of REAL st ( len b1 = len F & Sum b1 = 1 & ( for b2 being set holds ( not b2 in dom b1 or ( b1 . b2 = L . (F . b2) & 0 <= b1 . b2 ) ) ) ) take f = <*r,(1 - r)*>; ::_thesis: ( len f = len F & Sum f = 1 & ( for b1 being set holds ( not b1 in dom f or ( f . b1 = L . (F . b1) & 0 <= f . b1 ) ) ) ) len <*r,(1 - r)*> = 2 by FINSEQ_1:44 .= len <*u,v*> by FINSEQ_1:44 ; hence ( 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 A16, A11; ::_thesis: verum end; Sum L = (r * u) + ((1 - r) * v) by A6, A7, RLVECT_2:33; hence (r * u) + ((1 - r) * v) in M by A1, A5, A8; ::_thesis: verum end; supposeA17: u = v ; ::_thesis: (r * u) + ((1 - r) * v) in M consider L being Linear_Combination of {u} such that A18: L . u = 1 by RLVECT_4:37; reconsider L = L as Linear_Combination of N by A17, ENUMSET1:29; ex F being FinSequence of the carrier of V st ( F is one-to-one & rng F = Carrier L & 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 ) ) ) ) proof take <*u*> ; ::_thesis: ( <*u*> is one-to-one & rng <*u*> = Carrier L & ex f being FinSequence of REAL st ( len f = len <*u*> & Sum f = 1 & ( for n being Nat st n in dom f holds ( f . n = L . (<*u*> . n) & f . n >= 0 ) ) ) ) A19: ex f being FinSequence of REAL st ( len f = len <*u*> & Sum f = 1 & ( for n being Nat st n in dom f holds ( f . n = L . (<*u*> . n) & f . n >= 0 ) ) ) proof take <*rr*> ; ::_thesis: ( len <*rr*> = len <*u*> & Sum <*rr*> = 1 & ( for n being Nat st n in dom <*rr*> holds ( <*rr*> . n = L . (<*u*> . n) & <*rr*> . n >= 0 ) ) ) A20: for n being Element of NAT st n in dom <*rr*> holds ( <*rr*> . n = L . (<*u*> . n) & <*rr*> . n >= 0 ) proof let n be Element of NAT ; ::_thesis: ( n in dom <*rr*> implies ( <*rr*> . n = L . (<*u*> . n) & <*rr*> . n >= 0 ) ) assume n in dom <*rr*> ; ::_thesis: ( <*rr*> . n = L . (<*u*> . n) & <*rr*> . n >= 0 ) then n in {1} by FINSEQ_1:2, FINSEQ_1:38; then A21: n = 1 by TARSKI:def_1; then <*rr*> . n = 1 by FINSEQ_1:40 .= L . (<*u*> . n) by A18, A21, FINSEQ_1:40 ; hence ( <*rr*> . n = L . (<*u*> . n) & <*rr*> . n >= 0 ) by A21, FINSEQ_1:40; ::_thesis: verum end; len <*1*> = 1 by FINSEQ_1:39 .= len <*u*> by FINSEQ_1:39 ; hence ( len <*rr*> = len <*u*> & Sum <*rr*> = 1 & ( for n being Nat st n in dom <*rr*> holds ( <*rr*> . n = L . (<*u*> . n) & <*rr*> . n >= 0 ) ) ) by A20, FINSOP_1:11; ::_thesis: verum end; u in { w where w is Element of V : L . w <> 0 } by A18; then A22: u in Carrier L by RLVECT_2:def_4; v in { w where w is Element of V : L . w <> 0 } by A17, A18; then v in Carrier L by RLVECT_2:def_4; then ( Carrier L c= {u,v} & {u,v} c= Carrier L ) by A22, RLVECT_2:def_6, ZFMISC_1:32; then Carrier L = {u,v} by XBOOLE_0:def_10; then Carrier L = {u} by A17, ENUMSET1:29; hence ( <*u*> is one-to-one & rng <*u*> = Carrier L & ex f being FinSequence of REAL st ( len f = len <*u*> & Sum f = 1 & ( for n being Nat st n in dom f holds ( f . n = L . (<*u*> . n) & f . n >= 0 ) ) ) ) by A19, FINSEQ_1:38, FINSEQ_3:93; ::_thesis: verum end; then L is convex by CONVEX1:def_3; then A23: Sum L in M by A1, A5; (r * u) + ((1 - r) * v) = (r + (1 - r)) * u by A17, RLVECT_1:def_6 .= (0 + 1) * u ; hence (r * u) + ((1 - r) * v) in M by A18, A23, RLVECT_2:32; ::_thesis: verum end; end; end; hence (r * u) + ((1 - r) * v) in M ; ::_thesis: verum end; theorem :: CONVEX2:6 for V being RealLinearSpace for M being Subset of V holds ( ( 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 ) iff M is convex ) by Lm1, Lm2; definition let V be RealLinearSpace; let M be Subset of V; defpred S1[ set ] means \$1 is Linear_Combination of M; func LinComb M -> set means :: CONVEX2:def 1 for L being set holds ( L in it iff L is Linear_Combination of M ); existence ex b1 being set st for L being set holds ( L in b1 iff L is Linear_Combination of M ) proof consider A being set such that A1: for x being set holds ( x in A iff ( x in Funcs ( the carrier of V,REAL) & S1[x] ) ) from XBOOLE_0:sch_1(); take A ; ::_thesis: for L being set holds ( L in A iff L is Linear_Combination of M ) let L be set ; ::_thesis: ( L in A iff L is Linear_Combination of M ) thus ( L in A implies L is Linear_Combination of M ) by A1; ::_thesis: ( L is Linear_Combination of M implies L in A ) assume L is Linear_Combination of M ; ::_thesis: L in A hence L in A by A1; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for L being set holds ( L in b1 iff L is Linear_Combination of M ) ) & ( for L being set holds ( L in b2 iff L is Linear_Combination of M ) ) holds b1 = b2 proof thus for X1, X2 being set st ( for x being set holds ( x in X1 iff S1[x] ) ) & ( for x being set holds ( x in X2 iff S1[x] ) ) holds X1 = X2 from XBOOLE_0:sch_3(); ::_thesis: verum end; end; :: deftheorem defines LinComb CONVEX2:def_1_:_ for V being RealLinearSpace for M being Subset of V for b3 being set holds ( b3 = LinComb M iff for L being set holds ( L in b3 iff L is Linear_Combination of M ) ); registration let V be RealLinearSpace; cluster Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() convex for Linear_Combination of V; existence ex b1 being Linear_Combination of V st b1 is convex proof set u = the Element of V; consider L being Linear_Combination of { the Element of V} such that A1: L . the Element of V = 1 by RLVECT_4:37; reconsider L = L as Linear_Combination of V ; take L ; ::_thesis: L is convex L is convex proof take <* the Element of V*> ; :: according to CONVEX1:def_3 ::_thesis: ( <* the Element of V*> is one-to-one & rng <* the Element of V*> = Carrier L & ex b1 being FinSequence of REAL st ( len b1 = len <* the Element of V*> & Sum b1 = 1 & ( for b2 being set holds ( not b2 in dom b1 or ( b1 . b2 = L . (<* the Element of V*> . b2) & 0 <= b1 . b2 ) ) ) ) ) thus <* the Element of V*> is one-to-one by FINSEQ_3:93; ::_thesis: ( rng <* the Element of V*> = Carrier L & ex b1 being FinSequence of REAL st ( len b1 = len <* the Element of V*> & Sum b1 = 1 & ( for b2 being set holds ( not b2 in dom b1 or ( b1 . b2 = L . (<* the Element of V*> . b2) & 0 <= b1 . b2 ) ) ) ) ) the Element of V in { w where w is Element of V : L . w <> 0 } by A1; then the Element of V in Carrier L by RLVECT_2:def_4; then ( Carrier L c= { the Element of V} & { the Element of V} c= Carrier L ) by RLVECT_2:def_6, ZFMISC_1:31; hence Carrier L = { the Element of V} by XBOOLE_0:def_10 .= rng <* the Element of V*> by FINSEQ_1:38 ; ::_thesis: ex b1 being FinSequence of REAL st ( len b1 = len <* the Element of V*> & Sum b1 = 1 & ( for b2 being set holds ( not b2 in dom b1 or ( b1 . b2 = L . (<* the Element of V*> . b2) & 0 <= b1 . b2 ) ) ) ) take f = <*rr*>; ::_thesis: ( len f = len <* the Element of V*> & Sum f = 1 & ( for b1 being set holds ( not b1 in dom f or ( f . b1 = L . (<* the Element of V*> . b1) & 0 <= f . b1 ) ) ) ) A2: for n being Element of NAT st n in dom f holds ( f . n = L . (<* the Element of V*> . n) & f . n >= 0 ) proof let n be Element of NAT ; ::_thesis: ( n in dom f implies ( f . n = L . (<* the Element of V*> . n) & f . n >= 0 ) ) assume n in dom f ; ::_thesis: ( f . n = L . (<* the Element of V*> . n) & f . n >= 0 ) then n in {1} by FINSEQ_1:2, FINSEQ_1:38; then A3: n = 1 by TARSKI:def_1; then f . n = L . the Element of V by A1, FINSEQ_1:40 .= L . (<* the Element of V*> . n) by A3, FINSEQ_1:40 ; hence ( f . n = L . (<* the Element of V*> . n) & f . n >= 0 ) by A3, FINSEQ_1:40; ::_thesis: verum end; len <*1*> = 1 by FINSEQ_1:39 .= len <* the Element of V*> by FINSEQ_1:39 ; hence ( len f = len <* the Element of V*> & Sum f = 1 & ( for b1 being set holds ( not b1 in dom f or ( f . b1 = L . (<* the Element of V*> . b1) & 0 <= f . b1 ) ) ) ) by A2, FINSOP_1:11; ::_thesis: verum end; hence L is convex ; ::_thesis: verum end; end; definition let V be RealLinearSpace; mode Convex_Combination of V is convex Linear_Combination of V; end; registration let V be RealLinearSpace; let M be non empty Subset of V; cluster Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() convex for Linear_Combination of M; existence ex b1 being Linear_Combination of M st b1 is convex proof consider u being set such that A1: u in M by XBOOLE_0:def_1; reconsider u = u as Element of V by A1; consider L being Linear_Combination of {u} such that A2: L . u = 1 by RLVECT_4:37; {u} c= M by A1, ZFMISC_1:31; then reconsider L = L as Linear_Combination of M by RLVECT_2:21; take L ; ::_thesis: L is convex L is convex proof take <*u*> ; :: according to CONVEX1:def_3 ::_thesis: ( <*u*> is one-to-one & rng <*u*> = Carrier L & ex b1 being FinSequence of REAL st ( len b1 = len <*u*> & Sum b1 = 1 & ( for b2 being set holds ( not b2 in dom b1 or ( b1 . b2 = L . (<*u*> . b2) & 0 <= b1 . b2 ) ) ) ) ) thus <*u*> is one-to-one by FINSEQ_3:93; ::_thesis: ( rng <*u*> = Carrier L & ex b1 being FinSequence of REAL st ( len b1 = len <*u*> & Sum b1 = 1 & ( for b2 being set holds ( not b2 in dom b1 or ( b1 . b2 = L . (<*u*> . b2) & 0 <= b1 . b2 ) ) ) ) ) u in { w where w is Element of V : L . w <> 0 } by A2; then u in Carrier L by RLVECT_2:def_4; then ( Carrier L c= {u} & {u} c= Carrier L ) by RLVECT_2:def_6, ZFMISC_1:31; hence Carrier L = {u} by XBOOLE_0:def_10 .= rng <*u*> by FINSEQ_1:38 ; ::_thesis: ex b1 being FinSequence of REAL st ( len b1 = len <*u*> & Sum b1 = 1 & ( for b2 being set holds ( not b2 in dom b1 or ( b1 . b2 = L . (<*u*> . b2) & 0 <= b1 . b2 ) ) ) ) take f = <*rr*>; ::_thesis: ( len f = len <*u*> & Sum f = 1 & ( for b1 being set holds ( not b1 in dom f or ( f . b1 = L . (<*u*> . b1) & 0 <= f . b1 ) ) ) ) A3: for n being Element of NAT st n in dom f holds ( f . n = L . (<*u*> . n) & f . n >= 0 ) proof let n be Element of NAT ; ::_thesis: ( n in dom f implies ( f . n = L . (<*u*> . n) & f . n >= 0 ) ) assume n in dom f ; ::_thesis: ( f . n = L . (<*u*> . n) & f . n >= 0 ) then n in {1} by FINSEQ_1:2, FINSEQ_1:38; then A4: n = 1 by TARSKI:def_1; then f . n = L . u by A2, FINSEQ_1:40 .= L . (<*u*> . n) by A4, FINSEQ_1:40 ; hence ( f . n = L . (<*u*> . n) & f . n >= 0 ) by A4, FINSEQ_1:40; ::_thesis: verum end; len <*1*> = 1 by FINSEQ_1:39 .= len <*u*> by FINSEQ_1:39 ; hence ( len f = len <*u*> & Sum f = 1 & ( for b1 being set holds ( not b1 in dom f or ( f . b1 = L . (<*u*> . b1) & 0 <= f . b1 ) ) ) ) by A3, FINSOP_1:11; ::_thesis: verum end; hence L is convex ; ::_thesis: verum end; end; definition let V be RealLinearSpace; let M be non empty Subset of V; mode Convex_Combination of M is convex Linear_Combination of M; end; Lm3: for V being RealLinearSpace for W1, W2 being Subspace of V holds Up (W1 + W2) = (Up W1) + (Up W2) proof let V be RealLinearSpace; ::_thesis: for W1, W2 being Subspace of V holds Up (W1 + W2) = (Up W1) + (Up W2) let W1, W2 be Subspace of V; ::_thesis: Up (W1 + W2) = (Up W1) + (Up W2) A1: Up (W1 + W2) = the carrier of (W1 + W2) by RUSUB_4:def_5 .= { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } by RLSUB_2:def_1 ; for x being set st x in (Up W1) + (Up W2) holds x in Up (W1 + W2) proof let x be set ; ::_thesis: ( x in (Up W1) + (Up W2) implies x in Up (W1 + W2) ) assume x in (Up W1) + (Up W2) ; ::_thesis: x in Up (W1 + W2) then x in { (u + v) where u, v is Element of V : ( u in Up W1 & v in Up W2 ) } by RUSUB_4:def_9; then consider u, v being Element of V such that A2: x = u + v and A3: u in Up W1 and A4: v in Up W2 ; v in the carrier of W2 by A4, RUSUB_4:def_5; then A5: v in W2 by STRUCT_0:def_5; u in the carrier of W1 by A3, RUSUB_4:def_5; then u in W1 by STRUCT_0:def_5; hence x in Up (W1 + W2) by A1, A2, A5; ::_thesis: verum end; then A6: (Up W1) + (Up W2) c= Up (W1 + W2) by TARSKI:def_3; for x being set st x in Up (W1 + W2) holds x in (Up W1) + (Up W2) proof let x be set ; ::_thesis: ( x in Up (W1 + W2) implies x in (Up W1) + (Up W2) ) assume x in Up (W1 + W2) ; ::_thesis: x in (Up W1) + (Up W2) then consider v, u being VECTOR of V such that A7: x = v + u and A8: v in W1 and A9: u in W2 by A1; u in the carrier of W2 by A9, STRUCT_0:def_5; then A10: u in Up W2 by RUSUB_4:def_5; v in the carrier of W1 by A8, STRUCT_0:def_5; then v in Up W1 by RUSUB_4:def_5; then x in { (u9 + v9) where u9, v9 is Element of V : ( u9 in Up W1 & v9 in Up W2 ) } by A7, A10; hence x in (Up W1) + (Up W2) by RUSUB_4:def_9; ::_thesis: verum end; then Up (W1 + W2) c= (Up W1) + (Up W2) by TARSKI:def_3; hence Up (W1 + W2) = (Up W1) + (Up W2) by A6, XBOOLE_0:def_10; ::_thesis: verum end; Lm4: for V being RealLinearSpace for W1, W2 being Subspace of V holds Up (W1 /\ W2) = (Up W1) /\ (Up W2) proof let V be RealLinearSpace; ::_thesis: for W1, W2 being Subspace of V holds Up (W1 /\ W2) = (Up W1) /\ (Up W2) let W1, W2 be Subspace of V; ::_thesis: Up (W1 /\ W2) = (Up W1) /\ (Up W2) A1: Up (W1 /\ W2) = the carrier of (W1 /\ W2) by RUSUB_4:def_5 .= the carrier of W1 /\ the carrier of W2 by RLSUB_2:def_2 ; for x being set st x in (Up W1) /\ (Up W2) holds x in Up (W1 /\ W2) proof let x be set ; ::_thesis: ( x in (Up W1) /\ (Up W2) implies x in Up (W1 /\ W2) ) assume A2: x in (Up W1) /\ (Up W2) ; ::_thesis: x in Up (W1 /\ W2) then x in Up W2 by XBOOLE_0:def_4; then A3: x in the carrier of W2 by RUSUB_4:def_5; x in Up W1 by A2, XBOOLE_0:def_4; then x in the carrier of W1 by RUSUB_4:def_5; hence x in Up (W1 /\ W2) by A1, A3, XBOOLE_0:def_4; ::_thesis: verum end; then A4: (Up W1) /\ (Up W2) c= Up (W1 /\ W2) by TARSKI:def_3; for x being set st x in Up (W1 /\ W2) holds x in (Up W1) /\ (Up W2) proof let x be set ; ::_thesis: ( x in Up (W1 /\ W2) implies x in (Up W1) /\ (Up W2) ) assume A5: x in Up (W1 /\ W2) ; ::_thesis: x in (Up W1) /\ (Up W2) then x in the carrier of W2 by A1, XBOOLE_0:def_4; then A6: x in Up W2 by RUSUB_4:def_5; x in the carrier of W1 by A1, A5, XBOOLE_0:def_4; then x in Up W1 by RUSUB_4:def_5; hence x in (Up W1) /\ (Up W2) by A6, XBOOLE_0:def_4; ::_thesis: verum end; then Up (W1 /\ W2) c= (Up W1) /\ (Up W2) by TARSKI:def_3; hence Up (W1 /\ W2) = (Up W1) /\ (Up W2) by A4, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: CONVEX2:7 for V being RealLinearSpace for M being Subset of V holds Convex-Family M <> {} ; Lm5: for V being RealLinearSpace for L1, L2 being Convex_Combination of V for a, b being Real st a * b > 0 holds Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2)) proof let V be RealLinearSpace; ::_thesis: for L1, L2 being Convex_Combination of V for a, b being Real st a * b > 0 holds Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2)) let L1, L2 be Convex_Combination of V; ::_thesis: for a, b being Real st a * b > 0 holds Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2)) let a, b be Real; ::_thesis: ( a * b > 0 implies Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2)) ) assume a * b > 0 ; ::_thesis: Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2)) then A1: ( not ( a >= 0 & b <= 0 ) & not ( a <= 0 & b >= 0 ) ) by XREAL_1:131; then A2: Carrier L2 = Carrier (b * L2) by RLVECT_2:42; A3: Carrier L1 = Carrier (a * L1) by A1, RLVECT_2:42; for x being set st x in (Carrier (a * L1)) \/ (Carrier (b * L2)) holds x in Carrier ((a * L1) + (b * L2)) proof let x be set ; ::_thesis: ( x in (Carrier (a * L1)) \/ (Carrier (b * L2)) implies x in Carrier ((a * L1) + (b * L2)) ) assume A4: x in (Carrier (a * L1)) \/ (Carrier (b * L2)) ; ::_thesis: x in Carrier ((a * L1) + (b * L2)) now__::_thesis:_x_in_Carrier_((a_*_L1)_+_(b_*_L2)) percases ( x in Carrier (a * L1) or x in Carrier (b * L2) ) by A4, XBOOLE_0:def_3; supposeA5: x in Carrier (a * L1) ; ::_thesis: x in Carrier ((a * L1) + (b * L2)) then x in { v where v is Element of V : (a * L1) . v <> 0 } by RLVECT_2:def_4; then consider v being Element of V such that A6: v = x and A7: (a * L1) . v <> 0 ; A8: L1 . v > 0 by A3, A5, A6, CONVEX1:22; v in Carrier ((a * L1) + (b * L2)) proof now__::_thesis:_v_in_Carrier_((a_*_L1)_+_(b_*_L2)) percases ( v in Carrier L2 or not v in Carrier L2 ) ; supposeA9: v in Carrier L2 ; ::_thesis: v in Carrier ((a * L1) + (b * L2)) then A10: L2 . v > 0 by CONVEX1:22; now__::_thesis:_v_in_Carrier_((a_*_L1)_+_(b_*_L2)) percases ( ( a > 0 & b > 0 ) or ( a < 0 & b < 0 ) ) by A1; supposeA11: ( a > 0 & b > 0 ) ; ::_thesis: v in Carrier ((a * L1) + (b * L2)) then b * (L2 . v) > 0 by A10, XREAL_1:129; then (b * L2) . v > 0 by RLVECT_2:def_11; then A12: ((a * L1) . v) + ((b * L2) . v) > (a * L1) . v by XREAL_1:29; a * (L1 . v) > 0 by A8, A11, XREAL_1:129; then (a * L1) . v > 0 by RLVECT_2:def_11; then ((a * L1) + (b * L2)) . v > 0 by A12, RLVECT_2:def_10; hence v in Carrier ((a * L1) + (b * L2)) by RLVECT_2:19; ::_thesis: verum end; supposeA13: ( a < 0 & b < 0 ) ; ::_thesis: v in Carrier ((a * L1) + (b * L2)) then a * (L1 . v) < 0 by A3, A5, A6, CONVEX1:22, XREAL_1:132; then (a * L1) . v < 0 by RLVECT_2:def_11; then A14: ((a * L1) . v) + ((b * L2) . v) < (b * L2) . v by XREAL_1:30; b * (L2 . v) < 0 by A9, A13, CONVEX1:22, XREAL_1:132; then (b * L2) . v < 0 by RLVECT_2:def_11; then ((a * L1) + (b * L2)) . v < 0 by A14, RLVECT_2:def_10; hence v in Carrier ((a * L1) + (b * L2)) by RLVECT_2:19; ::_thesis: verum end; end; end; hence v in Carrier ((a * L1) + (b * L2)) ; ::_thesis: verum end; suppose not v in Carrier L2 ; ::_thesis: v in Carrier ((a * L1) + (b * L2)) then L2 . v = 0 by RLVECT_2:19; then b * (L2 . v) = 0 ; then (b * L2) . v = 0 by RLVECT_2:def_11; then ((a * L1) . v) + ((b * L2) . v) = (a * L1) . v ; then ((a * L1) + (b * L2)) . v <> 0 by A7, RLVECT_2:def_10; hence v in Carrier ((a * L1) + (b * L2)) by RLVECT_2:19; ::_thesis: verum end; end; end; hence v in Carrier ((a * L1) + (b * L2)) ; ::_thesis: verum end; hence x in Carrier ((a * L1) + (b * L2)) by A6; ::_thesis: verum end; supposeA15: x in Carrier (b * L2) ; ::_thesis: x in Carrier ((a * L1) + (b * L2)) then x in { v where v is Element of V : (b * L2) . v <> 0 } by RLVECT_2:def_4; then consider v being Element of V such that A16: v = x and A17: (b * L2) . v <> 0 ; A18: L2 . v > 0 by A2, A15, A16, CONVEX1:22; v in Carrier ((a * L1) + (b * L2)) proof now__::_thesis:_v_in_Carrier_((a_*_L1)_+_(b_*_L2)) percases ( v in Carrier L1 or not v in Carrier L1 ) ; supposeA19: v in Carrier L1 ; ::_thesis: v in Carrier ((a * L1) + (b * L2)) then A20: L1 . v > 0 by CONVEX1:22; now__::_thesis:_v_in_Carrier_((a_*_L1)_+_(b_*_L2)) percases ( ( a > 0 & b > 0 ) or ( a < 0 & b < 0 ) ) by A1; supposeA21: ( a > 0 & b > 0 ) ; ::_thesis: v in Carrier ((a * L1) + (b * L2)) then b * (L2 . v) > 0 by A18, XREAL_1:129; then (b * L2) . v > 0 by RLVECT_2:def_11; then A22: ((a * L1) . v) + ((b * L2) . v) > (a * L1) . v by XREAL_1:29; a * (L1 . v) > 0 by A20, A21, XREAL_1:129; then (a * L1) . v > 0 by RLVECT_2:def_11; then ((a * L1) + (b * L2)) . v > 0 by A22, RLVECT_2:def_10; hence v in Carrier ((a * L1) + (b * L2)) by RLVECT_2:19; ::_thesis: verum end; supposeA23: ( a < 0 & b < 0 ) ; ::_thesis: v in Carrier ((a * L1) + (b * L2)) then a * (L1 . v) < 0 by A19, CONVEX1:22, XREAL_1:132; then (a * L1) . v < 0 by RLVECT_2:def_11; then A24: ((a * L1) . v) + ((b * L2) . v) < (b * L2) . v by XREAL_1:30; b * (L2 . v) < 0 by A2, A15, A16, A23, CONVEX1:22, XREAL_1:132; then (b * L2) . v < 0 by RLVECT_2:def_11; then ((a * L1) + (b * L2)) . v < 0 by A24, RLVECT_2:def_10; hence v in Carrier ((a * L1) + (b * L2)) by RLVECT_2:19; ::_thesis: verum end; end; end; hence v in Carrier ((a * L1) + (b * L2)) ; ::_thesis: verum end; suppose not v in Carrier L1 ; ::_thesis: v in Carrier ((a * L1) + (b * L2)) then L1 . v = 0 by RLVECT_2:19; then a * (L1 . v) = 0 ; then (a * L1) . v = 0 by RLVECT_2:def_11; then ((a * L1) . v) + ((b * L2) . v) = (b * L2) . v ; then ((a * L1) + (b * L2)) . v <> 0 by A17, RLVECT_2:def_10; hence v in Carrier ((a * L1) + (b * L2)) by RLVECT_2:19; ::_thesis: verum end; end; end; hence v in Carrier ((a * L1) + (b * L2)) ; ::_thesis: verum end; hence x in Carrier ((a * L1) + (b * L2)) by A16; ::_thesis: verum end; end; end; hence x in Carrier ((a * L1) + (b * L2)) ; ::_thesis: verum end; then A25: (Carrier (a * L1)) \/ (Carrier (b * L2)) c= Carrier ((a * L1) + (b * L2)) by TARSKI:def_3; Carrier ((a * L1) + (b * L2)) c= (Carrier (a * L1)) \/ (Carrier (b * L2)) by RLVECT_2:37; hence Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2)) by A25, XBOOLE_0:def_10; ::_thesis: verum end; Lm6: for F, G being Function st F,G are_fiberwise_equipotent holds for x1, x2 being set st x1 in dom F & x2 in dom F & x1 <> x2 holds ex z1, z2 being set st ( z1 in dom G & z2 in dom G & z1 <> z2 & F . x1 = G . z1 & F . x2 = G . z2 ) proof let F, G be Function; ::_thesis: ( F,G are_fiberwise_equipotent implies for x1, x2 being set st x1 in dom F & x2 in dom F & x1 <> x2 holds ex z1, z2 being set st ( z1 in dom G & z2 in dom G & z1 <> z2 & F . x1 = G . z1 & F . x2 = G . z2 ) ) assume F,G are_fiberwise_equipotent ; ::_thesis: for x1, x2 being set st x1 in dom F & x2 in dom F & x1 <> x2 holds ex z1, z2 being set st ( z1 in dom G & z2 in dom G & z1 <> z2 & F . x1 = G . z1 & F . x2 = G . z2 ) then consider H being Function such that A1: dom H = dom F and A2: rng H = dom G and A3: H is one-to-one and A4: F = G * H by CLASSES1:77; let x1, x2 be set ; ::_thesis: ( x1 in dom F & x2 in dom F & x1 <> x2 implies ex z1, z2 being set st ( z1 in dom G & z2 in dom G & z1 <> z2 & F . x1 = G . z1 & F . x2 = G . z2 ) ) assume that A5: x1 in dom F and A6: x2 in dom F and A7: x1 <> x2 ; ::_thesis: ex z1, z2 being set st ( z1 in dom G & z2 in dom G & z1 <> z2 & F . x1 = G . z1 & F . x2 = G . z2 ) A8: ( H . x1 in dom G & H . x2 in dom G ) by A5, A6, A1, A2, FUNCT_1:3; A9: F . x2 = G . (H . x2) by A6, A4, FUNCT_1:12; ( H . x1 <> H . x2 & F . x1 = G . (H . x1) ) by A5, A6, A7, A1, A3, A4, FUNCT_1:12, FUNCT_1:def_4; hence ex z1, z2 being set st ( z1 in dom G & z2 in dom G & z1 <> z2 & F . x1 = G . z1 & F . x2 = G . z2 ) by A8, A9; ::_thesis: verum end; Lm7: for V being RealLinearSpace for L being Linear_Combination of V for A being Subset of V st A c= Carrier L holds ex L1 being Linear_Combination of V st Carrier L1 = A proof let V be RealLinearSpace; ::_thesis: for L being Linear_Combination of V for A being Subset of V st A c= Carrier L holds ex L1 being Linear_Combination of V st Carrier L1 = A let L be Linear_Combination of V; ::_thesis: for A being Subset of V st A c= Carrier L holds ex L1 being Linear_Combination of V st Carrier L1 = A let A be Subset of V; ::_thesis: ( A c= Carrier L implies ex L1 being Linear_Combination of V st Carrier L1 = A ) consider F being Function such that A1: L = F and A2: dom F = the carrier of V and A3: rng F c= REAL by FUNCT_2:def_2; defpred S1[ set , set ] means ( ( \$1 in A implies \$2 = F . \$1 ) & ( not \$1 in A implies \$2 = 0 ) ); A4: for x being set st x in the carrier of V holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in the carrier of V implies ex y being set st S1[x,y] ) assume x in the carrier of V ; ::_thesis: ex y being set st S1[x,y] now__::_thesis:_ex_y_being_set_st_S1[x,y] percases ( x in A or not x in A ) ; suppose x in A ; ::_thesis: ex y being set st S1[x,y] hence ex y being set st S1[x,y] ; ::_thesis: verum end; suppose not x in A ; ::_thesis: ex y being set st S1[x,y] hence ex y being set st S1[x,y] ; ::_thesis: verum end; end; end; hence ex y being set st S1[x,y] ; ::_thesis: verum end; consider L1 being Function such that A5: ( dom L1 = the carrier of V & ( for x being set st x in the carrier of V holds S1[x,L1 . x] ) ) from CLASSES1:sch_1(A4); for y being set st y in rng L1 holds y in REAL proof let y be set ; ::_thesis: ( y in rng L1 implies y in REAL ) assume y in rng L1 ; ::_thesis: y in REAL then consider x being set such that A6: x in dom L1 and A7: y = L1 . x by FUNCT_1:def_3; reconsider x = x as Element of V by A5, A6; now__::_thesis:_y_in_REAL percases ( x in A or not x in A ) ; supposeA8: x in A ; ::_thesis: y in REAL A9: F . x in rng F by A2, FUNCT_1:3; y = F . x by A5, A7, A8; hence y in REAL by A3, A9; ::_thesis: verum end; suppose not x in A ; ::_thesis: y in REAL then L1 . x = 0 by A5; hence y in REAL by A7; ::_thesis: verum end; end; end; hence y in REAL ; ::_thesis: verum end; then rng L1 c= REAL by TARSKI:def_3; then A10: L1 is Element of Funcs ( the carrier of V,REAL) by A5, FUNCT_2:def_2; assume A11: A c= Carrier L ; ::_thesis: ex L1 being Linear_Combination of V st Carrier L1 = A then reconsider A = A as finite Subset of V by FINSET_1:1; for v being Element of V st not v in A holds L1 . v = 0 by A5; then reconsider L1 = L1 as Linear_Combination of V by A10, RLVECT_2:def_3; for v being set st v in Carrier L1 holds v in A proof let v be set ; ::_thesis: ( v in Carrier L1 implies v in A ) assume A12: v in Carrier L1 ; ::_thesis: v in A then reconsider v = v as Element of V ; L1 . v <> 0 by A12, RLVECT_2:19; hence v in A by A5; ::_thesis: verum end; then A13: Carrier L1 c= A by TARSKI:def_3; take L1 ; ::_thesis: Carrier L1 = A for v being set st v in A holds v in Carrier L1 proof let v be set ; ::_thesis: ( v in A implies v in Carrier L1 ) assume A14: v in A ; ::_thesis: v in Carrier L1 then reconsider v = v as Element of V ; ( L1 . v = F . v & L . v <> 0 ) by A11, A5, A14, RLVECT_2:19; hence v in Carrier L1 by A1, RLVECT_2:19; ::_thesis: verum end; then A c= Carrier L1 by TARSKI:def_3; hence Carrier L1 = A by A13, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th8: :: CONVEX2:8 for V being RealLinearSpace for L1, L2 being Convex_Combination of V for r being Real st 0 < r & r < 1 holds (r * L1) + ((1 - r) * L2) is Convex_Combination of V proof let V be RealLinearSpace; ::_thesis: for L1, L2 being Convex_Combination of V for r being Real st 0 < r & r < 1 holds (r * L1) + ((1 - r) * L2) is Convex_Combination of V let L1, L2 be Convex_Combination of V; ::_thesis: for r being Real st 0 < r & r < 1 holds (r * L1) + ((1 - r) * L2) is Convex_Combination of V let r be Real; ::_thesis: ( 0 < r & r < 1 implies (r * L1) + ((1 - r) * L2) is Convex_Combination of V ) assume that A1: 0 < r and A2: r < 1 ; ::_thesis: (r * L1) + ((1 - r) * L2) is Convex_Combination of V A3: Carrier (r * L1) = Carrier L1 by A1, RLVECT_2:42; set Mid = (Carrier (r * L1)) /\ (Carrier ((1 - r) * L2)); set L = (r * L1) + ((1 - r) * L2); consider F2 being FinSequence of the carrier of V such that A4: F2 is one-to-one and A5: rng F2 = Carrier L2 and A6: ex f being FinSequence of REAL st ( len f = len F2 & Sum f = 1 & ( for n being Nat st n in dom f holds ( f . n = L2 . (F2 . n) & f . n >= 0 ) ) ) by CONVEX1:def_3; set Btm = (Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier (r * L1)); set Top = (Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier ((1 - r) * L2)); consider F1 being FinSequence of the carrier of V such that A7: F1 is one-to-one and A8: rng F1 = Carrier L1 and A9: ex f being FinSequence of REAL st ( len f = len F1 & Sum f = 1 & ( for n being Nat st n in dom f holds ( f . n = L1 . (F1 . n) & f . n >= 0 ) ) ) by CONVEX1:def_3; consider Lt being Linear_Combination of V such that A10: Carrier Lt = (Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier ((1 - r) * L2)) by Lm7, XBOOLE_1:36; A11: r - r < 1 - r by A2, XREAL_1:9; then A12: Carrier ((1 - r) * L2) = Carrier L2 by RLVECT_2:42; A13: r * (1 - r) > 0 by A1, A11, XREAL_1:129; then A14: Carrier ((r * L1) + ((1 - r) * L2)) = (Carrier (r * L1)) \/ (Carrier ((1 - r) * L2)) by Lm5; then consider Lm being Linear_Combination of V such that A15: Carrier Lm = (Carrier (r * L1)) /\ (Carrier ((1 - r) * L2)) by Lm7, XBOOLE_1:29; consider Lb being Linear_Combination of V such that A16: Carrier Lb = (Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier (r * L1)) by Lm7, XBOOLE_1:36; consider Ft being FinSequence of the carrier of V such that A17: Ft is one-to-one and A18: rng Ft = Carrier Lt and Sum Lt = Sum (Lt (#) Ft) by RLVECT_2:def_8; consider Fb being FinSequence of the carrier of V such that A19: Fb is one-to-one and A20: rng Fb = Carrier Lb and Sum Lb = Sum (Lb (#) Fb) by RLVECT_2:def_8; consider Fm being FinSequence of the carrier of V such that A21: Fm is one-to-one and A22: rng Fm = Carrier Lm and Sum Lm = Sum (Lm (#) Fm) by RLVECT_2:def_8; A23: rng (Ft ^ Fm) = (rng Ft) \/ (rng Fm) by FINSEQ_1:31 .= (((Carrier L1) \/ (Carrier L2)) \ (Carrier L2)) \/ ((Carrier L1) /\ (Carrier L2)) by A13, A3, A12, A10, A15, A18, A22, Lm5 .= (((Carrier L1) \ (Carrier L2)) \/ ((Carrier L2) \ (Carrier L2))) \/ ((Carrier L1) /\ (Carrier L2)) by XBOOLE_1:42 .= (((Carrier L1) \ (Carrier L2)) \/ {}) \/ ((Carrier L1) /\ (Carrier L2)) by XBOOLE_1:37 .= (Carrier L1) \ ((Carrier L2) \ (Carrier L2)) by XBOOLE_1:52 .= (Carrier L1) \ {} by XBOOLE_1:37 .= rng F1 by A8 ; A24: rng Ft misses rng Fm by A10, A15, A18, A22, XBOOLE_1:17, XBOOLE_1:85; then A25: Ft ^ Fm is one-to-one by A17, A21, FINSEQ_3:91; set F = (Ft ^ Fm) ^ Fb; consider f2 being FinSequence of REAL such that A26: len f2 = len F2 and A27: Sum f2 = 1 and A28: for n being Nat st n in dom f2 holds ( f2 . n = L2 . (F2 . n) & f2 . n >= 0 ) by A6; deffunc H1( set ) -> set = L1 . (Ft . \$1); consider ft being FinSequence such that A29: ( len ft = len Ft & ( for j being Nat st j in dom ft holds ft . j = H1(j) ) ) from FINSEQ_1:sch_2(); rng ft c= REAL proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ft or y in REAL ) consider L1f being Function such that A30: L1 = L1f and A31: dom L1f = the carrier of V and A32: rng L1f c= REAL by FUNCT_2:def_2; assume y in rng ft ; ::_thesis: y in REAL then consider x being set such that A33: x in dom ft and A34: ft . x = y by FUNCT_1:def_3; reconsider x = x as Element of NAT by A33; A35: ft . x = L1 . (Ft . x) by A29, A33; x in Seg (len Ft) by A29, A33, FINSEQ_1:def_3; then x in dom Ft by FINSEQ_1:def_3; then A36: Ft . x in rng Ft by FUNCT_1:3; rng Ft c= the carrier of V by FINSEQ_1:def_4; then reconsider Ftx = Ft . x as Element of V by A36; Ftx in dom L1f by A31; then ft . x in rng L1f by A35, A30, FUNCT_1:3; hence y in REAL by A34, A32; ::_thesis: verum end; then reconsider ft = ft as FinSequence of REAL by FINSEQ_1:def_4; deffunc H2( set ) -> set = L1 . (Fm . \$1); consider fm1 being FinSequence such that A37: ( len fm1 = len Fm & ( for j being Nat st j in dom fm1 holds fm1 . j = H2(j) ) ) from FINSEQ_1:sch_2(); rng fm1 c= REAL proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng fm1 or y in REAL ) consider L1f being Function such that A38: L1 = L1f and A39: dom L1f = the carrier of V and A40: rng L1f c= REAL by FUNCT_2:def_2; assume y in rng fm1 ; ::_thesis: y in REAL then consider x being set such that A41: x in dom fm1 and A42: fm1 . x = y by FUNCT_1:def_3; reconsider x = x as Element of NAT by A41; A43: fm1 . x = L1 . (Fm . x) by A37, A41; x in Seg (len Fm) by A37, A41, FINSEQ_1:def_3; then x in dom Fm by FINSEQ_1:def_3; then A44: Fm . x in rng Fm by FUNCT_1:3; rng Fm c= the carrier of V by FINSEQ_1:def_4; then reconsider Fmx = Fm . x as Element of V by A44; Fmx in dom L1f by A39; then fm1 . x in rng L1f by A43, A38, FUNCT_1:3; hence y in REAL by A42, A40; ::_thesis: verum end; then reconsider fm1 = fm1 as FinSequence of REAL by FINSEQ_1:def_4; deffunc H3( set ) -> set = L2 . (Fm . \$1); consider fm2 being FinSequence such that A45: ( len fm2 = len Fm & ( for j being Nat st j in dom fm2 holds fm2 . j = H3(j) ) ) from FINSEQ_1:sch_2(); A46: for x being set st x in dom (ft ^ fm1) holds (ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x) proof let x be set ; ::_thesis: ( x in dom (ft ^ fm1) implies (ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x) ) assume A47: x in dom (ft ^ fm1) ; ::_thesis: (ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x) then reconsider n = x as Element of NAT ; now__::_thesis:_(ft_^_fm1)_._x_=_L1_._((Ft_^_Fm)_._x) percases ( n in dom ft or ex m being Nat st ( m in dom fm1 & n = (len ft) + m ) ) by A47, FINSEQ_1:25; supposeA48: n in dom ft ; ::_thesis: (ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x) then n in Seg (len Ft) by A29, FINSEQ_1:def_3; then A49: n in dom Ft by FINSEQ_1:def_3; ft . n = L1 . (Ft . n) by A29, A48; then (ft ^ fm1) . n = L1 . (Ft . n) by A48, FINSEQ_1:def_7; hence (ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x) by A49, FINSEQ_1:def_7; ::_thesis: verum end; suppose ex m being Nat st ( m in dom fm1 & n = (len ft) + m ) ; ::_thesis: (ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x) then consider m being Element of NAT such that A50: m in dom fm1 and A51: n = (len ft) + m ; m in Seg (len Fm) by A37, A50, FINSEQ_1:def_3; then A52: m in dom Fm by FINSEQ_1:def_3; (ft ^ fm1) . n = fm1 . m by A50, A51, FINSEQ_1:def_7 .= L1 . (Fm . m) by A37, A50 ; hence (ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x) by A29, A51, A52, FINSEQ_1:def_7; ::_thesis: verum end; end; end; hence (ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x) ; ::_thesis: verum end; for x being set holds ( x in dom (ft ^ fm1) iff ( x in dom (Ft ^ Fm) & (Ft ^ Fm) . x in dom L1 ) ) proof let x be set ; ::_thesis: ( x in dom (ft ^ fm1) iff ( x in dom (Ft ^ Fm) & (Ft ^ Fm) . x in dom L1 ) ) A53: len (ft ^ fm1) = (len ft) + (len fm1) by FINSEQ_1:22 .= len (Ft ^ Fm) by A29, A37, FINSEQ_1:22 ; A54: dom (ft ^ fm1) = Seg (len (ft ^ fm1)) by FINSEQ_1:def_3 .= dom (Ft ^ Fm) by A53, FINSEQ_1:def_3 ; ( x in dom (ft ^ fm1) implies (Ft ^ Fm) . x in dom L1 ) proof assume x in dom (ft ^ fm1) ; ::_thesis: (Ft ^ Fm) . x in dom L1 then (Ft ^ Fm) . x in rng (Ft ^ Fm) by A54, FUNCT_1:3; then A55: (Ft ^ Fm) . x in (Carrier Lt) \/ (Carrier Lm) by A18, A22, FINSEQ_1:31; dom L1 = the carrier of V by FUNCT_2:92; hence (Ft ^ Fm) . x in dom L1 by A55; ::_thesis: verum end; hence ( x in dom (ft ^ fm1) iff ( x in dom (Ft ^ Fm) & (Ft ^ Fm) . x in dom L1 ) ) by A54; ::_thesis: verum end; then A56: ft ^ fm1 = L1 * (Ft ^ Fm) by A46, FUNCT_1:10; A57: dom L2 = the carrier of V by FUNCT_2:92; A58: for x being set holds ( x in dom f2 iff ( x in dom F2 & F2 . x in dom L2 ) ) proof let x be set ; ::_thesis: ( x in dom f2 iff ( x in dom F2 & F2 . x in dom L2 ) ) A59: now__::_thesis:_(_x_in_dom_f2_implies_(_x_in_dom_F2_&_F2_._x_in_dom_L2_)_) assume x in dom f2 ; ::_thesis: ( x in dom F2 & F2 . x in dom L2 ) then x in Seg (len F2) by A26, FINSEQ_1:def_3; hence x in dom F2 by FINSEQ_1:def_3; ::_thesis: F2 . x in dom L2 then F2 . x in rng F2 by FUNCT_1:3; hence F2 . x in dom L2 by A5, A57; ::_thesis: verum end; now__::_thesis:_(_x_in_dom_F2_&_F2_._x_in_dom_L2_implies_x_in_dom_f2_) assume that A60: x in dom F2 and F2 . x in dom L2 ; ::_thesis: x in dom f2 x in Seg (len F2) by A60, FINSEQ_1:def_3; hence x in dom f2 by A26, FINSEQ_1:def_3; ::_thesis: verum end; hence ( x in dom f2 iff ( x in dom F2 & F2 . x in dom L2 ) ) by A59; ::_thesis: verum end; deffunc H4( set ) -> set = L2 . (Fb . \$1); consider fb being FinSequence such that A61: ( len fb = len Fb & ( for j being Nat st j in dom fb holds fb . j = H4(j) ) ) from FINSEQ_1:sch_2(); rng fm2 c= REAL proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng fm2 or y in REAL ) consider L2f being Function such that A62: L2 = L2f and A63: dom L2f = the carrier of V and A64: rng L2f c= REAL by FUNCT_2:def_2; assume y in rng fm2 ; ::_thesis: y in REAL then consider x being set such that A65: x in dom fm2 and A66: fm2 . x = y by FUNCT_1:def_3; reconsider x = x as Element of NAT by A65; A67: fm2 . x = L2 . (Fm . x) by A45, A65; x in Seg (len Fm) by A45, A65, FINSEQ_1:def_3; then x in dom Fm by FINSEQ_1:def_3; then A68: Fm . x in rng Fm by FUNCT_1:3; rng Fm c= the carrier of V by FINSEQ_1:def_4; then reconsider Fmx = Fm . x as Element of V by A68; Fmx in dom L2f by A63; then fm2 . x in rng L2f by A67, A62, FUNCT_1:3; hence y in REAL by A66, A64; ::_thesis: verum end; then reconsider fm2 = fm2 as FinSequence of REAL by FINSEQ_1:def_4; A69: len (r * fm1) = len fm1 by RVSUM_1:117 .= len ((1 - r) * fm2) by A37, A45, RVSUM_1:117 ; rng fb c= REAL proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng fb or y in REAL ) consider L2f being Function such that A70: L2 = L2f and A71: dom L2f = the carrier of V and A72: rng L2f c= REAL by FUNCT_2:def_2; assume y in rng fb ; ::_thesis: y in REAL then consider x being set such that A73: x in dom fb and A74: fb . x = y by FUNCT_1:def_3; reconsider x = x as Element of NAT by A73; A75: fb . x = L2 . (Fb . x) by A61, A73; x in Seg (len Fb) by A61, A73, FINSEQ_1:def_3; then x in dom Fb by FINSEQ_1:def_3; then A76: Fb . x in rng Fb by FUNCT_1:3; rng Fb c= the carrier of V by FINSEQ_1:def_4; then reconsider Fbx = Fb . x as Element of V by A76; Fbx in dom L2f by A71; then fb . x in rng L2f by A75, A70, FUNCT_1:3; hence y in REAL by A74, A72; ::_thesis: verum end; then reconsider fb = fb as FinSequence of REAL by FINSEQ_1:def_4; set f = ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb); consider f1 being FinSequence of REAL such that A77: len f1 = len F1 and A78: Sum f1 = 1 and A79: for n being Nat st n in dom f1 holds ( f1 . n = L1 . (F1 . n) & f1 . n >= 0 ) by A9; len (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) = (len ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2)))) + (len ((1 - r) * fb)) by FINSEQ_1:22 .= ((len (r * ft)) + (len ((r * fm1) + ((1 - r) * fm2)))) + (len ((1 - r) * fb)) by FINSEQ_1:22 .= ((len ft) + (len ((r * fm1) + ((1 - r) * fm2)))) + (len ((1 - r) * fb)) by RVSUM_1:117 .= ((len ft) + (len ((r * fm1) + ((1 - r) * fm2)))) + (len fb) by RVSUM_1:117 .= ((len ft) + (len (r * fm1))) + (len fb) by A69, INTEGRA5:2 .= ((len Ft) + (len Fm)) + (len Fb) by A29, A37, A61, RVSUM_1:117 .= (len (Ft ^ Fm)) + (len Fb) by FINSEQ_1:22 ; then A80: len (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) = len ((Ft ^ Fm) ^ Fb) by FINSEQ_1:22; A81: dom L1 = the carrier of V by FUNCT_2:92; A82: for x being set holds ( x in dom f1 iff ( x in dom F1 & F1 . x in dom L1 ) ) proof let x be set ; ::_thesis: ( x in dom f1 iff ( x in dom F1 & F1 . x in dom L1 ) ) A83: now__::_thesis:_(_x_in_dom_f1_implies_(_x_in_dom_F1_&_F1_._x_in_dom_L1_)_) assume x in dom f1 ; ::_thesis: ( x in dom F1 & F1 . x in dom L1 ) then x in Seg (len F1) by A77, FINSEQ_1:def_3; hence x in dom F1 by FINSEQ_1:def_3; ::_thesis: F1 . x in dom L1 then F1 . x in rng F1 by FUNCT_1:3; hence F1 . x in dom L1 by A8, A81; ::_thesis: verum end; now__::_thesis:_(_x_in_dom_F1_&_F1_._x_in_dom_L1_implies_x_in_dom_f1_) assume that A84: x in dom F1 and F1 . x in dom L1 ; ::_thesis: x in dom f1 x in Seg (len F1) by A84, FINSEQ_1:def_3; hence x in dom f1 by A77, FINSEQ_1:def_3; ::_thesis: verum end; hence ( x in dom f1 iff ( x in dom F1 & F1 . x in dom L1 ) ) by A83; ::_thesis: verum end; A85: rng (Ft ^ Fm) = (Carrier Lt) \/ (Carrier Lm) by A18, A22, FINSEQ_1:31; for x being set st x in dom f1 holds f1 . x = L1 . (F1 . x) by A79; then A86: f1 = L1 * F1 by A82, FUNCT_1:10; Ft ^ Fm is one-to-one by A17, A21, A24, FINSEQ_3:91; then A87: F1,Ft ^ Fm are_fiberwise_equipotent by A7, A23, RFINSEQ:26; then dom F1 = dom (Ft ^ Fm) by RFINSEQ:3; then A88: Sum f1 = Sum (ft ^ fm1) by A8, A87, A81, A86, A85, A56, CLASSES1:83, RFINSEQ:9; A89: rng (Fm ^ Fb) = (Carrier Lm) \/ (Carrier Lb) by A22, A20, FINSEQ_1:31; for x being set st x in dom f2 holds f2 . x = L2 . (F2 . x) by A28; then A90: f2 = L2 * F2 by A58, FUNCT_1:10; A91: rng (Fm ^ Fb) = ((Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier (r * L1))) \/ ((Carrier (r * L1)) /\ (Carrier ((1 - r) * L2))) by A15, A16, A22, A20, FINSEQ_1:31 .= (((Carrier L1) \/ (Carrier L2)) \ (Carrier L1)) \/ ((Carrier L1) /\ (Carrier L2)) by A13, A3, A12, Lm5 .= (((Carrier L1) \ (Carrier L1)) \/ ((Carrier L2) \ (Carrier L1))) \/ ((Carrier L1) /\ (Carrier L2)) by XBOOLE_1:42 .= (((Carrier L2) \ (Carrier L1)) \/ {}) \/ ((Carrier L1) /\ (Carrier L2)) by XBOOLE_1:37 .= (Carrier L2) \ ((Carrier L1) \ (Carrier L1)) by XBOOLE_1:52 .= (Carrier L2) \ {} by XBOOLE_1:37 .= rng F2 by A5 ; for n being Element of NAT st n in dom (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) holds ( (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) & (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 ) proof let n be Element of NAT ; ::_thesis: ( n in dom (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) implies ( (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) & (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 ) ) assume A92: n in dom (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) ; ::_thesis: ( (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) & (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 ) now__::_thesis:_(_(((r_*_ft)_^_((r_*_fm1)_+_((1_-_r)_*_fm2)))_^_((1_-_r)_*_fb))_._n_=_((r_*_L1)_+_((1_-_r)_*_L2))_._(((Ft_^_Fm)_^_Fb)_._n)_&_(((r_*_ft)_^_((r_*_fm1)_+_((1_-_r)_*_fm2)))_^_((1_-_r)_*_fb))_._n_>=_0_) percases ( n in dom ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) or ex m being Nat st ( m in dom ((1 - r) * fb) & n = (len ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2)))) + m ) ) by A92, FINSEQ_1:25; supposeA93: n in dom ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ; ::_thesis: ( (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) & (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 ) then A94: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) . n by FINSEQ_1:def_7; now__::_thesis:_(_(((r_*_ft)_^_((r_*_fm1)_+_((1_-_r)_*_fm2)))_^_((1_-_r)_*_fb))_._n_=_((r_*_L1)_+_((1_-_r)_*_L2))_._(((Ft_^_Fm)_^_Fb)_._n)_&_(((r_*_ft)_^_((r_*_fm1)_+_((1_-_r)_*_fm2)))_^_((1_-_r)_*_fb))_._n_>=_0_) percases ( n in dom (r * ft) or ex k being Nat st ( k in dom ((r * fm1) + ((1 - r) * fm2)) & n = (len (r * ft)) + k ) ) by A93, FINSEQ_1:25; supposeA95: n in dom (r * ft) ; ::_thesis: ( (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) & (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 ) len ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) = (len (r * ft)) + (len ((r * fm1) + ((1 - r) * fm2))) by FINSEQ_1:22 .= (len ft) + (len ((r * fm1) + ((1 - r) * fm2))) by RVSUM_1:117 .= (len ft) + (len (r * fm1)) by A69, INTEGRA5:2 .= (len Ft) + (len Fm) by A29, A37, RVSUM_1:117 .= len (Ft ^ Fm) by FINSEQ_1:22 ; then n in Seg (len (Ft ^ Fm)) by A93, FINSEQ_1:def_3; then n in dom (Ft ^ Fm) by FINSEQ_1:def_3; then A96: (Ft ^ Fm) . n = ((Ft ^ Fm) ^ Fb) . n by FINSEQ_1:def_7; A97: n in dom ft by A95, VALUED_1:def_5; then n in Seg (len Ft) by A29, FINSEQ_1:def_3; then A98: n in dom Ft by FINSEQ_1:def_3; then A99: Ft . n in Carrier Lt by A18, FUNCT_1:3; then reconsider Ftn = Ft . n as Element of V ; A100: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = (r * ft) . n by A94, A95, FINSEQ_1:def_7 .= r * (ft . n) by RVSUM_1:44 .= r * (L1 . (Ft . n)) by A29, A97 ; not Ft . n in Carrier L2 by A12, A10, A99, XBOOLE_0:def_5; then L2 . Ftn = 0 by RLVECT_2:19; then (1 - r) * (L2 . Ftn) = 0 ; then ((1 - r) * L2) . Ftn = 0 by RLVECT_2:def_11; then (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) . Ftn) + (((1 - r) * L2) . Ftn) by A100, RLVECT_2:def_11 .= ((r * L1) + ((1 - r) * L2)) . (Ft . n) by RLVECT_2:def_10 ; hence (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) by A98, A96, FINSEQ_1:def_7; ::_thesis: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 A101: rng Ft c= rng (Ft ^ Fm) by FINSEQ_1:29; Ft . n in rng Ft by A98, FUNCT_1:3; then consider m9 being set such that A102: m9 in dom F1 and A103: F1 . m9 = Ft . n by A23, A101, FUNCT_1:def_3; reconsider m9 = m9 as Element of NAT by A102; m9 in Seg (len f1) by A77, A102, FINSEQ_1:def_3; then m9 in dom f1 by FINSEQ_1:def_3; then ( f1 . m9 = L1 . (F1 . m9) & f1 . m9 >= 0 ) by A79; hence (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 by A1, A100, A103, XREAL_1:127; ::_thesis: verum end; suppose ex k being Nat st ( k in dom ((r * fm1) + ((1 - r) * fm2)) & n = (len (r * ft)) + k ) ; ::_thesis: ( (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) & (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 ) then consider m being Element of NAT such that A104: m in dom ((r * fm1) + ((1 - r) * fm2)) and A105: n = (len (r * ft)) + m ; len (r * fm1) = len fm1 by RVSUM_1:117 .= len ((1 - r) * fm2) by A37, A45, RVSUM_1:117 ; then A106: len ((r * fm1) + ((1 - r) * fm2)) = len (r * fm1) by INTEGRA5:2 .= len fm1 by RVSUM_1:117 ; then A107: m in dom Fm by A37, A104, FINSEQ_3:29; then A108: Fm . m in rng Fm by FUNCT_1:3; then reconsider Fmm = Fm . m as Element of V by A22; A109: m in dom fm1 by A104, A106, FINSEQ_3:29; A110: m in dom fm2 by A37, A45, A104, A106, FINSEQ_3:29; A111: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * fm1) + ((1 - r) * fm2)) . m by A94, A104, A105, FINSEQ_1:def_7 .= ((r * fm1) . m) + (((1 - r) * fm2) . m) by A104, VALUED_1:def_1 .= (r * (fm1 . m)) + (((1 - r) * fm2) . m) by RVSUM_1:44 .= (r * (fm1 . m)) + ((1 - r) * (fm2 . m)) by RVSUM_1:44 .= (r * (L1 . (Fm . m))) + ((1 - r) * (fm2 . m)) by A37, A109 .= (r * (L1 . (Fm . m))) + ((1 - r) * (L2 . (Fm . m))) by A45, A110 ; len ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) = (len (r * ft)) + (len ((r * fm1) + ((1 - r) * fm2))) by FINSEQ_1:22 .= (len ft) + (len ((r * fm1) + ((1 - r) * fm2))) by RVSUM_1:117 .= (len ft) + (len (r * fm1)) by A69, INTEGRA5:2 .= (len Ft) + (len Fm) by A29, A37, RVSUM_1:117 .= len (Ft ^ Fm) by FINSEQ_1:22 ; then n in Seg (len (Ft ^ Fm)) by A93, FINSEQ_1:def_3; then n in dom (Ft ^ Fm) by FINSEQ_1:def_3; then A112: (Ft ^ Fm) . n = ((Ft ^ Fm) ^ Fb) . n by FINSEQ_1:def_7; A113: len (r * ft) = len Ft by A29, RVSUM_1:117; ( r * (L1 . Fmm) = (r * L1) . (Fm . m) & (1 - r) * (L2 . Fmm) = ((1 - r) * L2) . (Fm . m) ) by RLVECT_2:def_11; then (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (Fm . m) by A111, RLVECT_2:def_10; hence (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) by A105, A107, A112, A113, FINSEQ_1:def_7; ::_thesis: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 rng Fm c= rng (Ft ^ Fm) by FINSEQ_1:30; then consider m9 being set such that A114: m9 in dom F1 and A115: F1 . m9 = Fm . m by A23, A108, FUNCT_1:def_3; reconsider m9 = m9 as Element of NAT by A114; m9 in Seg (len F1) by A114, FINSEQ_1:def_3; then m9 in dom f1 by A77, FINSEQ_1:def_3; then ( f1 . m9 = L1 . (F1 . m9) & f1 . m9 >= 0 ) by A79; then A116: r * (L1 . (Fm . m)) >= 0 by A1, A115, XREAL_1:127; rng Fm c= rng (Fm ^ Fb) by FINSEQ_1:29; then consider m9 being set such that A117: m9 in dom F2 and A118: F2 . m9 = Fm . m by A91, A108, FUNCT_1:def_3; reconsider m9 = m9 as Element of NAT by A117; m9 in Seg (len F2) by A117, FINSEQ_1:def_3; then m9 in dom f2 by A26, FINSEQ_1:def_3; then ( f2 . m9 = L2 . (F2 . m9) & f2 . m9 >= 0 ) by A28; then (1 - r) * (L2 . (Fm . m)) >= 0 by A11, A118, XREAL_1:127; then (r * (L1 . (Fm . m))) + ((1 - r) * (L2 . (Fm . m))) >= 0 + 0 by A116, XREAL_1:7; hence (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 by A111; ::_thesis: verum end; end; end; hence ( (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) & (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 ) ; ::_thesis: verum end; suppose ex m being Nat st ( m in dom ((1 - r) * fb) & n = (len ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2)))) + m ) ; ::_thesis: ( (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) & (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 ) then consider m being Element of NAT such that A119: m in dom ((1 - r) * fb) and A120: n = (len ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2)))) + m ; A121: m in dom fb by A119, VALUED_1:def_5; then m in Seg (len Fb) by A61, FINSEQ_1:def_3; then A122: m in dom Fb by FINSEQ_1:def_3; then A123: Fb . m in rng Fb by FUNCT_1:3; then reconsider Fbm = Fb . m as Element of V by A20; A124: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((1 - r) * fb) . m by A119, A120, FINSEQ_1:def_7 .= (1 - r) * (fb . m) by RVSUM_1:44 .= (1 - r) * (L2 . (Fb . m)) by A61, A121 ; A125: len ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) = (len (r * ft)) + (len ((r * fm1) + ((1 - r) * fm2))) by FINSEQ_1:22 .= (len ft) + (len ((r * fm1) + ((1 - r) * fm2))) by RVSUM_1:117 .= (len ft) + (len (r * fm1)) by A69, INTEGRA5:2 .= (len Ft) + (len Fm) by A29, A37, RVSUM_1:117 .= len (Ft ^ Fm) by FINSEQ_1:22 ; not Fb . m in Carrier L1 by A3, A16, A20, A123, XBOOLE_0:def_5; then L1 . Fbm = 0 by RLVECT_2:19; then r * (L1 . Fbm) = 0 ; then (r * L1) . Fbm = 0 by RLVECT_2:def_11; then (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) . Fbm) + (((1 - r) * L2) . Fbm) by A124, RLVECT_2:def_11 .= ((r * L1) + ((1 - r) * L2)) . (Fb . m) by RLVECT_2:def_10 ; hence (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) by A120, A122, A125, FINSEQ_1:def_7; ::_thesis: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 rng Fb c= rng (Fm ^ Fb) by FINSEQ_1:30; then consider m9 being set such that A126: m9 in dom F2 and A127: F2 . m9 = Fb . m by A91, A123, FUNCT_1:def_3; reconsider m9 = m9 as Element of NAT by A126; m9 in Seg (len F2) by A126, FINSEQ_1:def_3; then m9 in dom f2 by A26, FINSEQ_1:def_3; then ( f2 . m9 = L2 . (F2 . m9) & f2 . m9 >= 0 ) by A28; hence (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 by A11, A124, A127, XREAL_1:127; ::_thesis: verum end; end; end; hence ( (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) & (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 ) ; ::_thesis: verum end; then A128: for n being Nat st n in dom (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) holds ( (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) & (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 ) ; A129: rng Fb = (Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier L1) by A1, A16, A20, RLVECT_2:42; then rng (Ft ^ Fm) misses rng Fb by A8, A23, XBOOLE_1:79; then A130: (Ft ^ Fm) ^ Fb is one-to-one by A19, A25, FINSEQ_3:91; A131: for x being set st x in dom (fm2 ^ fb) holds (fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x) proof let x be set ; ::_thesis: ( x in dom (fm2 ^ fb) implies (fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x) ) assume A132: x in dom (fm2 ^ fb) ; ::_thesis: (fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x) then reconsider n = x as Element of NAT ; now__::_thesis:_(fm2_^_fb)_._x_=_L2_._((Fm_^_Fb)_._x) percases ( n in dom fm2 or ex m being Nat st ( m in dom fb & n = (len fm2) + m ) ) by A132, FINSEQ_1:25; supposeA133: n in dom fm2 ; ::_thesis: (fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x) then n in Seg (len Fm) by A45, FINSEQ_1:def_3; then A134: n in dom Fm by FINSEQ_1:def_3; fm2 . n = L2 . (Fm . n) by A45, A133; then (fm2 ^ fb) . n = L2 . (Fm . n) by A133, FINSEQ_1:def_7; hence (fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x) by A134, FINSEQ_1:def_7; ::_thesis: verum end; suppose ex m being Nat st ( m in dom fb & n = (len fm2) + m ) ; ::_thesis: (fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x) then consider m being Element of NAT such that A135: m in dom fb and A136: n = (len fm2) + m ; m in Seg (len Fb) by A61, A135, FINSEQ_1:def_3; then A137: m in dom Fb by FINSEQ_1:def_3; (fm2 ^ fb) . n = fb . m by A135, A136, FINSEQ_1:def_7 .= L2 . (Fb . m) by A61, A135 ; hence (fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x) by A45, A136, A137, FINSEQ_1:def_7; ::_thesis: verum end; end; end; hence (fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x) ; ::_thesis: verum end; for x being set holds ( x in dom (fm2 ^ fb) iff ( x in dom (Fm ^ Fb) & (Fm ^ Fb) . x in dom L2 ) ) proof let x be set ; ::_thesis: ( x in dom (fm2 ^ fb) iff ( x in dom (Fm ^ Fb) & (Fm ^ Fb) . x in dom L2 ) ) A138: len (fm2 ^ fb) = (len fm2) + (len fb) by FINSEQ_1:22 .= len (Fm ^ Fb) by A45, A61, FINSEQ_1:22 ; A139: dom (fm2 ^ fb) = Seg (len (fm2 ^ fb)) by FINSEQ_1:def_3 .= dom (Fm ^ Fb) by A138, FINSEQ_1:def_3 ; ( x in dom (fm2 ^ fb) implies (Fm ^ Fb) . x in dom L2 ) proof assume x in dom (fm2 ^ fb) ; ::_thesis: (Fm ^ Fb) . x in dom L2 then (Fm ^ Fb) . x in rng (Fm ^ Fb) by A139, FUNCT_1:3; then A140: (Fm ^ Fb) . x in (Carrier Lm) \/ (Carrier Lb) by A22, A20, FINSEQ_1:31; dom L2 = the carrier of V by FUNCT_2:92; hence (Fm ^ Fb) . x in dom L2 by A140; ::_thesis: verum end; hence ( x in dom (fm2 ^ fb) iff ( x in dom (Fm ^ Fb) & (Fm ^ Fb) . x in dom L2 ) ) by A139; ::_thesis: verum end; then A141: fm2 ^ fb = L2 * (Fm ^ Fb) by A131, FUNCT_1:10; rng Fm misses rng Fb by A15, A16, A22, A20, XBOOLE_1:17, XBOOLE_1:85; then Fm ^ Fb is one-to-one by A21, A19, FINSEQ_3:91; then A142: F2,Fm ^ Fb are_fiberwise_equipotent by A4, A91, RFINSEQ:26; then dom F2 = dom (Fm ^ Fb) by RFINSEQ:3; then A143: Sum f2 = Sum (fm2 ^ fb) by A5, A142, A57, A90, A89, A141, CLASSES1:83, RFINSEQ:9; A144: Sum (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) = (Sum ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2)))) + (Sum ((1 - r) * fb)) by RVSUM_1:75 .= ((Sum (r * ft)) + (Sum ((r * fm1) + ((1 - r) * fm2)))) + (Sum ((1 - r) * fb)) by RVSUM_1:75 .= ((r * (Sum ft)) + (Sum ((r * fm1) + ((1 - r) * fm2)))) + (Sum ((1 - r) * fb)) by RVSUM_1:87 .= ((r * (Sum ft)) + (Sum ((r * fm1) + ((1 - r) * fm2)))) + ((1 - r) * (Sum fb)) by RVSUM_1:87 .= ((r * (Sum ft)) + ((Sum (r * fm1)) + (Sum ((1 - r) * fm2)))) + ((1 - r) * (Sum fb)) by A69, INTEGRA5:2 .= ((r * (Sum ft)) + ((r * (Sum fm1)) + (Sum ((1 - r) * fm2)))) + ((1 - r) * (Sum fb)) by RVSUM_1:87 .= ((r * (Sum ft)) + ((r * (Sum fm1)) + ((1 - r) * (Sum fm2)))) + ((1 - r) * (Sum fb)) by RVSUM_1:87 .= (r * ((Sum ft) + (Sum fm1))) + ((1 - r) * ((Sum fm2) + (Sum fb))) .= (r * (Sum (ft ^ fm1))) + ((1 - r) * ((Sum fm2) + (Sum fb))) by RVSUM_1:75 .= (r * 1) + ((1 - r) * 1) by A78, A27, A88, A143, RVSUM_1:75 .= 0 + 1 ; rng ((Ft ^ Fm) ^ Fb) = (Carrier L1) \/ ((Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier L1)) by A8, A23, A129, FINSEQ_1:31 .= (Carrier L1) \/ (Carrier ((r * L1) + ((1 - r) * L2))) by XBOOLE_1:39 .= Carrier ((r * L1) + ((1 - r) * L2)) by A3, A14, XBOOLE_1:7, XBOOLE_1:12 ; hence (r * L1) + ((1 - r) * L2) is Convex_Combination of V by A130, A144, A80, A128, CONVEX1:def_3; ::_thesis: verum end; theorem :: CONVEX2:9 for V being RealLinearSpace for M being non empty Subset of V for L1, L2 being Convex_Combination of M for r being Real st 0 < r & r < 1 holds (r * L1) + ((1 - r) * L2) is Convex_Combination of M proof let V be RealLinearSpace; ::_thesis: for M being non empty Subset of V for L1, L2 being Convex_Combination of M for r being Real st 0 < r & r < 1 holds (r * L1) + ((1 - r) * L2) is Convex_Combination of M let M be non empty Subset of V; ::_thesis: for L1, L2 being Convex_Combination of M for r being Real st 0 < r & r < 1 holds (r * L1) + ((1 - r) * L2) is Convex_Combination of M let L1, L2 be Convex_Combination of M; ::_thesis: for r being Real st 0 < r & r < 1 holds (r * L1) + ((1 - r) * L2) is Convex_Combination of M let r be Real; ::_thesis: ( 0 < r & r < 1 implies (r * L1) + ((1 - r) * L2) is Convex_Combination of M ) A1: ( r * L1 is Linear_Combination of M & (1 - r) * L2 is Linear_Combination of M ) by RLVECT_2:44; assume ( 0 < r & r < 1 ) ; ::_thesis: (r * L1) + ((1 - r) * L2) is Convex_Combination of M hence (r * L1) + ((1 - r) * L2) is Convex_Combination of M by A1, Th8, RLVECT_2:38; ::_thesis: verum end; begin theorem :: CONVEX2:10 for V being RealLinearSpace for W1, W2 being Subspace of V holds Up (W1 + W2) = (Up W1) + (Up W2) by Lm3; theorem :: CONVEX2:11 for V being RealLinearSpace for W1, W2 being Subspace of V holds Up (W1 /\ W2) = (Up W1) /\ (Up W2) by Lm4; theorem :: CONVEX2:12 for V being RealLinearSpace for L1, L2 being Convex_Combination of V for a, b being Real st a * b > 0 holds Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2)) by Lm5; theorem :: CONVEX2:13 for F, G being Function st F,G are_fiberwise_equipotent holds for x1, x2 being set st x1 in dom F & x2 in dom F & x1 <> x2 holds ex z1, z2 being set st ( z1 in dom G & z2 in dom G & z1 <> z2 & F . x1 = G . z1 & F . x2 = G . z2 ) by Lm6; theorem :: CONVEX2:14 for V being RealLinearSpace for L being Linear_Combination of V for A being Subset of V st A c= Carrier L holds ex L1 being Linear_Combination of V st Carrier L1 = A by Lm7;