convex2.miz



    begin

    reconsider rr = 1 as Element of REAL by XREAL_0:def 1;

    set ff = <*rr*>;

    theorem :: CONVEX2:1

    for V be non empty RLSStruct, M,N be convex Subset of V holds (M /\ N) is convex;

    theorem :: CONVEX2:2

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

    proof

      let V be RealUnitarySpace-like non empty UNITSTR;

      let M be Subset of V;

      let F be FinSequence of the carrier of V;

      let B be FinSequence of REAL ;

      assume

       A1: M = { u where u be VECTOR of V : for i be Element of NAT st i in (( dom F) /\ ( dom B)) holds ex v be VECTOR of V st v = (F . i) & (u .|. v) <= (B . i) };

      let u1,v1 be VECTOR of V;

      let r be Real;

      assume that

       A2: 0 < r and

       A3: r < 1 and

       A4: u1 in M and

       A5: v1 in M;

      consider v9 be VECTOR of V such that

       A6: v1 = v9 and

       A7: for i be Element of NAT st i in (( dom F) /\ ( dom B)) holds ex v be VECTOR of V st v = (F . i) & (v9 .|. v) <= (B . i) by A1, A5;

      consider u9 be VECTOR of V such that

       A8: u1 = u9 and

       A9: for i be Element of NAT st i in (( dom F) /\ ( dom B)) holds ex v be VECTOR of V st v = (F . i) & (u9 .|. v) <= (B . i) by A1, A4;

      for i be Element of NAT st i in (( dom F) /\ ( dom B)) holds ex v be 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 ;

        assume

         A11: i in (( dom F) /\ ( dom B));

        reconsider b = (B . i) as Real;

        consider x be VECTOR of V such that

         A12: x = (F . i) and

         A13: (u9 .|. x) <= b by A9, A11;

        take v = x;

        

         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 be 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 thesis by A12;

      end;

      hence thesis by A1;

    end;

    theorem :: CONVEX2:3

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

    proof

      let V be RealUnitarySpace-like non empty UNITSTR;

      let M be Subset of V;

      let F be FinSequence of the carrier of V;

      let B be FinSequence of REAL ;

      assume

       A1: M = { u where u be VECTOR of V : for i be Element of NAT st i in (( dom F) /\ ( dom B)) holds ex v be VECTOR of V st v = (F . i) & (u .|. v) < (B . i) };

      let u1,v1 be VECTOR of V;

      let r be Real;

      assume that

       A2: 0 < r and

       A3: r < 1 and

       A4: u1 in M and

       A5: v1 in M;

      consider v9 be VECTOR of V such that

       A6: v1 = v9 and

       A7: for i be Element of NAT st i in (( dom F) /\ ( dom B)) holds ex v be VECTOR of V st v = (F . i) & (v9 .|. v) < (B . i) by A1, A5;

      consider u9 be VECTOR of V such that

       A8: u1 = u9 and

       A9: for i be Element of NAT st i in (( dom F) /\ ( dom B)) holds ex v be VECTOR of V st v = (F . i) & (u9 .|. v) < (B . i) by A1, A4;

      for i be Element of NAT st i in (( dom F) /\ ( dom B)) holds ex v be 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 ;

        assume

         A11: i in (( dom F) /\ ( dom B));

        reconsider b = (B . i) as Real;

        consider x be VECTOR of V such that

         A12: x = (F . i) and

         A13: (u9 .|. x) < b by A9, A11;

        take v = x;

        

         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 be 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 thesis by A12;

      end;

      hence thesis by A1;

    end;

    theorem :: CONVEX2:4

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

    proof

      let V be RealUnitarySpace-like non empty UNITSTR;

      let M be Subset of V;

      let F be FinSequence of the carrier of V;

      let B be FinSequence of REAL ;

      assume

       A1: M = { u where u be VECTOR of V : for i be Element of NAT st i in (( dom F) /\ ( dom B)) holds ex v be VECTOR of V st v = (F . i) & (u .|. v) >= (B . i) };

      let u1,v1 be VECTOR of V;

      let r be Real;

      assume that

       A2: 0 < r and

       A3: r < 1 and

       A4: u1 in M and

       A5: v1 in M;

      consider v9 be VECTOR of V such that

       A6: v1 = v9 and

       A7: for i be Element of NAT st i in (( dom F) /\ ( dom B)) holds ex v be VECTOR of V st v = (F . i) & (v9 .|. v) >= (B . i) by A1, A5;

      consider u9 be VECTOR of V such that

       A8: u1 = u9 and

       A9: for i be Element of NAT st i in (( dom F) /\ ( dom B)) holds ex v be VECTOR of V st v = (F . i) & (u9 .|. v) >= (B . i) by A1, A4;

      for i be Element of NAT st i in (( dom F) /\ ( dom B)) holds ex v be 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 ;

        assume

         A11: i in (( dom F) /\ ( dom B));

        reconsider b = (B . i) as Real;

        consider x be VECTOR of V such that

         A12: x = (F . i) and

         A13: (u9 .|. x) >= b by A9, A11;

        take v = x;

        

         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 be 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 thesis by A12;

      end;

      hence thesis by A1;

    end;

    theorem :: CONVEX2:5

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

    proof

      let V be RealUnitarySpace-like non empty UNITSTR;

      let M be Subset of V;

      let F be FinSequence of the carrier of V;

      let B be FinSequence of REAL ;

      assume

       A1: M = { u where u be VECTOR of V : for i be Element of NAT st i in (( dom F) /\ ( dom B)) holds ex v be VECTOR of V st v = (F . i) & (u .|. v) > (B . i) };

      let u1,v1 be VECTOR of V;

      let r be Real;

      assume that

       A2: 0 < r and

       A3: r < 1 and

       A4: u1 in M and

       A5: v1 in M;

      consider v9 be VECTOR of V such that

       A6: v1 = v9 and

       A7: for i be Element of NAT st i in (( dom F) /\ ( dom B)) holds ex v be VECTOR of V st v = (F . i) & (v9 .|. v) > (B . i) by A1, A5;

      consider u9 be VECTOR of V such that

       A8: u1 = u9 and

       A9: for i be Element of NAT st i in (( dom F) /\ ( dom B)) holds ex v be VECTOR of V st v = (F . i) & (u9 .|. v) > (B . i) by A1, A4;

      for i be Element of NAT st i in (( dom F) /\ ( dom B)) holds ex v be 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 ;

        assume

         A11: i in (( dom F) /\ ( dom B));

        reconsider b = (B . i) as Real;

        consider x be VECTOR of V such that

         A12: x = (F . i) and

         A13: (u9 .|. x) > b by A9, A11;

        take v = x;

        

         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 be 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 thesis by A12;

      end;

      hence thesis by A1;

    end;

    

     Lm1: for V be RealLinearSpace, M be convex Subset of V holds for N be Subset of V, L be Linear_Combination of N st L is convex & N c= M holds ( Sum L) in M

    proof

      let V be RealLinearSpace;

      let M be convex Subset of V;

      let N be Subset of V;

      let L be Linear_Combination of N;

      assume that

       A1: L is convex and

       A2: N c= M;

      consider F be FinSequence of the carrier of V such that

       A3: F is one-to-one and

       A4: ( rng F) = ( Carrier L) and

       A5: ex f be FinSequence of REAL st ( len f) = ( len F) & ( Sum f) = 1 & for n be Nat st n in ( dom f) holds (f . n) = (L . (F . n)) & (f . n) >= 0 by A1;

      consider f be FinSequence of REAL such that

       A6: ( len f) = ( len F) and

       A7: ( Sum f) = 1 and

       A8: for n be 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 zero Element of NAT by A3, A4, FINSEQ_4: 62;

      

       A10: ( len (L (#) F)) = ( len F) by RLVECT_2:def 7;

      defpred P[ 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 be non zero Nat st P[k] holds P[(k + 1)]

      proof

        let k be non zero Nat;

        

         A13: k >= 1 by NAT_1: 14;

        assume

         A14: ((1 / ( Sum ( mid (f,1,k)))) * ( Sum ( mid ((L (#) F),1,k)))) in M;

        now

          per cases ;

            suppose

             A15: k >= ( len f);

            

             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 thesis by A14, A17, A18, A16;

          end;

            suppose

             A19: k < ( len f);

            ( 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 be Element of NAT st i in ( dom ( mid (f,1,k))) & 0 < (( mid (f,1,k)) . i)

            proof

              take 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 be Element of V : (L . v) <> 0 } by RLVECT_2:def 4;

              then

               A24: ex v be Element of V st v = (F . 1) & (L . v) <> 0 ;

              1 in ( Seg ( len ( mid (f,1,k)))) by A13, A20;

              hence thesis by A13, A19, A23, A24, FINSEQ_1:def 3, FINSEQ_6: 123;

            end;

            

             A25: for i be 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;

              assume i in ( dom <*(( mid (f,1,(k + 1))) . (k + 1))*>);

              then i in ( Seg 1) by FINSEQ_1: 38;

              then i = 1 by FINSEQ_1: 2, TARSKI:def 1;

              hence thesis by A20, FINSEQ_1: 40;

            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 be Nat st i in ( dom ( mid (f,1,k))) holds 0 <= (( mid (f,1,k)) . i)

            proof

              let i be Nat;

              assume i in ( dom ( mid (f,1,k)));

              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 thesis by A8, A30;

            end;

            then

             A31: r1 > 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 be 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;

              

               A35: ( mid (f,1,k)) = (f | k) by FINSEQ_6: 116, NAT_1: 14;

              assume

               A36: i in ( dom ( mid (f,1,k)));

              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 thesis by A26, A39, A40, FINSEQ_4: 70;

            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 / (r1 + r2)) * r1) = (r1 / (r1 + r2)) by XCMPLX_1: 99;

            

             A50: w2 in M & r2 > 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 w2 = (F . (k + 1)) by PARTFUN1:def 6;

              then

               A53: w2 in ( Carrier L) by A4, A52, FUNCT_1:def 3;

              ( Carrier L) c= N by RLVECT_2:def 6;

              hence w2 in M by A2, A53;

              w2 in { v where v be Element of V : (L . v) <> 0 } by A53, RLVECT_2:def 4;

              then ex v be Element of V st v = w2 & (L . v) <> 0 ;

              hence thesis by A52, A51, PARTFUN1:def 6;

            end;

            then (r1 + r2) > r1 by XREAL_1: 29;

            then

             A54: ((1 / (r1 + r2)) * r1) < 1 by A31, A49, XREAL_1: 189;

            

             A55: (r1 + r2) > ( 0 + 0 qua Nat) by A31, A50;

            then (1 / (r1 + r2)) > 0 by XREAL_1: 139;

            then

             A56: 0 < ((1 / (r1 + r2)) * r1) 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 be 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;

              

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

              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 thesis by A48, A66, A67, FINSEQ_4: 70;

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

              assume i in ( dom <*(( mid ((L (#) F),1,(k + 1))) . (k + 1))*>);

              then i in ( Seg 1) by FINSEQ_1: 38;

              then i = 1 by FINSEQ_1: 2, TARSKI:def 1;

              hence thesis by A70, FINSEQ_1: 40;

            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 / (r1 + r2)) * (w1 + (r2 * w2))) by A47, A69, FVSUM_1: 71

            .= ((1 / (r1 + r2)) * ((1 * w1) + (r2 * w2))) by RLVECT_1:def 8

            .= ((1 / (r1 + r2)) * (((r1 * (1 / r1)) * w1) + (r2 * w2))) by A31, XCMPLX_1: 106

            .= ((1 / (r1 + r2)) * ((r1 * ((1 / r1) * w1)) + (r2 * w2))) by RLVECT_1:def 7

            .= (((1 / (r1 + r2)) * (r1 * ((1 / r1) * w1))) + ((1 / (r1 + r2)) * (r2 * w2))) by RLVECT_1:def 5

            .= ((((1 / (r1 + r2)) * r1) * ((1 / r1) * w1)) + ((1 / (r1 + r2)) * (r2 * w2))) by RLVECT_1:def 7

            .= ((((1 / (r1 + r2)) * r1) * ((1 / r1) * w1)) + (((1 / (r1 + r2)) * r2) * w2)) by RLVECT_1:def 7;

            (1 - ((1 / (r1 + r2)) * r1)) = (((r1 + r2) * (1 / (r1 + r2))) - ((1 / (r1 + r2)) * r1)) by A55, XCMPLX_1: 106

            .= (((r1 + r2) - r1) * (1 / (r1 + r2)));

            hence thesis by A14, A50, A56, A54, A72, CONVEX1:def 2;

          end;

        end;

        hence thesis;

      end;

      ( len F) > 0 by A3, A4, A9, FINSEQ_4: 62;

      then

       A73: ( len F) >= ( 0 + 1) by NAT_1: 13;

      

       A74: P[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;

        ( 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 be Element of V : (L . v) <> 0 } by A4, RLVECT_2:def 4;

        then

         A84: ex v2 be 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 thesis by A4, A81, A83, A77;

      end;

      for k be non zero Nat holds P[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 thesis by A3, A4, A6, A86, A10, RLVECT_2:def 8;

    end;

    reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

    

     Lm2: for V be RealLinearSpace, M be Subset of V st for N be Subset of V, L be 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;

      let M be Subset of V;

      assume

       A1: for N be Subset of V, L be Linear_Combination of N st L is convex & N c= M holds ( Sum L) in M;

      let u,v be VECTOR of V;

      let rr be Real;

      reconsider r = rr as Real;

      assume that

       A2: 0 < rr and

       A3: rr < 1 and

       A4: u in M & v in M;

      set N = {u, v};

      

       A5: N c= M by A4, ZFMISC_1: 32;

      reconsider N as Subset of V;

      now

        per cases ;

          suppose

           A6: u <> v;

          consider L be Linear_Combination of {u, v} such that

           A7: (L . u) = r & (L . v) = (1 - r) by A6, RLVECT_4: 38;

          reconsider 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 be Element of V : (L . w) <> 0 } by A7;

            then

             A10: v in ( Carrier L) by RLVECT_2:def 4;

            

             A11: for n be 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 ;

              assume n in ( dom <*r, (1 - r)*>);

              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

                per cases by A12, TARSKI:def 2;

                  suppose

                   A13: n = 1;

                  then (L . ( <*u, v*> . n)) = r by A7, FINSEQ_1: 44;

                  hence thesis by A2, A13, FINSEQ_1: 44;

                end;

                  suppose

                   A14: n = 2;

                  then (L . ( <*u, v*> . n)) = (1 - r) by A7, FINSEQ_1: 44;

                  hence thesis by A9, A14, FINSEQ_1: 44;

                end;

              end;

              hence thesis;

            end;

            u in { w where w be 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*>;

            

             A16: ( Sum <*r, (1 - r)*>) = (r + (1 - r)) by RVSUM_1: 77

            .= 1;

            thus F is one-to-one by A6, FINSEQ_3: 94;

            

            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;

            reconsider r as Element of REAL by XREAL_0:def 1;

            reconsider jr = (1 - r) as Element of REAL by XREAL_0:def 1;

            take f = <*r, jr*>;

            ( 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 be Nat st n in ( dom f) holds (f . n) = (L . (F . n)) & (f . n) >= 0 by A16, A11;

          end;

          ( Sum L) = ((r * u) + ((1 - r) * v)) by A6, A7, RLVECT_2: 33;

          hence thesis by A1, A5, A8;

        end;

          suppose

           A17: u = v;

          consider L be Linear_Combination of {u} such that

           A18: (L . u) = jj by RLVECT_4: 37;

          reconsider L as Linear_Combination of N by A17, ENUMSET1: 29;

          ex F be FinSequence of the carrier of V st F is one-to-one & ( rng F) = ( Carrier L) & ex f be FinSequence of REAL st ( len f) = ( len F) & ( Sum f) = 1 & for n be Nat st n in ( dom f) holds (f . n) = (L . (F . n)) & (f . n) >= 0

          proof

            take <*u*>;

            

             A19: ex f be FinSequence of REAL st ( len f) = ( len <*u*>) & ( Sum f) = 1 & for n be Nat st n in ( dom f) holds (f . n) = (L . ( <*u*> . n)) & (f . n) >= 0

            proof

              take ff;

              

               A20: for n be Element of NAT st n in ( dom ff) holds (ff . n) = (L . ( <*u*> . n)) & (ff . n) >= 0

              proof

                let n be Element of NAT ;

                assume n in ( dom ff);

                then n in {1} by FINSEQ_1: 2, FINSEQ_1: 38;

                then

                 A21: n = 1 by TARSKI:def 1;

                

                then (ff . n) = 1 by FINSEQ_1: 40

                .= (L . ( <*u*> . n)) by A18, A21, FINSEQ_1: 40;

                hence thesis;

              end;

              ( len <*1*>) = 1 by FINSEQ_1: 39

              .= ( len <*u*>) by FINSEQ_1: 39;

              hence thesis by A20, FINSOP_1: 11;

            end;

            u in { w where w be Element of V : (L . w) <> 0 } by A18;

            then

             A22: u in ( Carrier L) by RLVECT_2:def 4;

            v in { w where w be 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 thesis by A19, FINSEQ_1: 38, FINSEQ_3: 93;

          end;

          then L is convex;

          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 thesis by A18, A23, RLVECT_2: 32;

        end;

      end;

      hence thesis;

    end;

    theorem :: CONVEX2:6

    for V be RealLinearSpace, M be Subset of V holds (for N be Subset of V, L be 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, M be Subset of V;

      defpred P[ object] means $1 is Linear_Combination of M;

      :: CONVEX2:def1

      func LinComb (M) -> set means for L be object holds L in it iff L is Linear_Combination of M;

      existence

      proof

        consider A be set such that

         A1: for x be object holds x in A iff x in ( Funcs (the carrier of V, REAL )) & P[x] from XBOOLE_0:sch 1;

        take A;

        let L be object;

        thus L in A implies L is Linear_Combination of M by A1;

        assume L is Linear_Combination of M;

        hence thesis by A1;

      end;

      uniqueness

      proof

        thus for X1,X2 be set st (for x be object holds x in X1 iff P[x]) & (for x be object holds x in X2 iff P[x]) holds X1 = X2 from XBOOLE_0:sch 3;

      end;

    end

    registration

      let V be RealLinearSpace;

      cluster convex for Linear_Combination of V;

      existence

      proof

        set u = the Element of V;

        consider L be Linear_Combination of {u} such that

         A1: (L . u) = jj by RLVECT_4: 37;

        reconsider L as Linear_Combination of V;

        take L;

        L is convex

        proof

          take <*u*>;

          thus <*u*> is one-to-one by FINSEQ_3: 93;

          u in { w where w be Element of V : (L . w) <> 0 } by A1;

          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;

          take f = ff;

          

           A2: for n be Element of NAT st n in ( dom f) holds (f . n) = (L . ( <*u*> . n)) & (f . n) >= 0

          proof

            let n be Element of NAT ;

            assume n in ( dom f);

            then n in {1} by FINSEQ_1: 2, FINSEQ_1: 38;

            then

             A3: n = 1 by TARSKI:def 1;

            

            then (f . n) = (L . u) by A1, FINSEQ_1: 40

            .= (L . ( <*u*> . n)) by A3, FINSEQ_1: 40;

            hence thesis;

          end;

          ( len <*1*>) = 1 by FINSEQ_1: 39

          .= ( len <*u*>) by FINSEQ_1: 39;

          hence thesis by A2, FINSOP_1: 11;

        end;

        hence thesis;

      end;

    end

    definition

      let V be RealLinearSpace;

      mode Convex_Combination of V is convex Linear_Combination of V;

    end

    registration

      let V be RealLinearSpace, M be non empty Subset of V;

      cluster convex for Linear_Combination of M;

      existence

      proof

        consider u be object such that

         A1: u in M by XBOOLE_0:def 1;

        reconsider u as Element of V by A1;

        consider L be Linear_Combination of {u} such that

         A2: (L . u) = jj by RLVECT_4: 37;

         {u} c= M by A1, ZFMISC_1: 31;

        then

        reconsider L as Linear_Combination of M by RLVECT_2: 21;

        take L;

        L is convex

        proof

          take <*u*>;

          thus <*u*> is one-to-one by FINSEQ_3: 93;

          u in { w where w be 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;

          take f = ff;

          

           A3: for n be Element of NAT st n in ( dom f) holds (f . n) = (L . ( <*u*> . n)) & (f . n) >= 0

          proof

            let n be Element of NAT ;

            assume n in ( dom f);

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

          end;

          ( len <*1*>) = 1 by FINSEQ_1: 39

          .= ( len <*u*>) by FINSEQ_1: 39;

          hence thesis by A3, FINSOP_1: 11;

        end;

        hence thesis;

      end;

    end

    definition

      let V be RealLinearSpace, M be non empty Subset of V;

      mode Convex_Combination of M is convex Linear_Combination of M;

    end

    

     Lm3: for V be RealLinearSpace, W1,W2 be Subspace of V holds ( Up (W1 + W2)) = (( Up W1) + ( Up W2))

    proof

      let V be RealLinearSpace;

      let W1,W2 be Subspace of V;

      

       A1: ( Up (W1 + W2)) = the carrier of (W1 + W2) by RUSUB_4:def 5

      .= { (v + u) where u,v be VECTOR of V : v in W1 & u in W2 } by RLSUB_2:def 1;

      for x be object st x in (( Up W1) + ( Up W2)) holds x in ( Up (W1 + W2))

      proof

        let x be object;

        assume x in (( Up W1) + ( Up W2));

        then x in { (u + v) where u,v be Element of V : u in ( Up W1) & v in ( Up W2) } by RUSUB_4:def 9;

        then

        consider u,v be 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 thesis by A1, A2, A5;

      end;

      then

       A6: (( Up W1) + ( Up W2)) c= ( Up (W1 + W2));

      for x be object st x in ( Up (W1 + W2)) holds x in (( Up W1) + ( Up W2))

      proof

        let x be object;

        assume x in ( Up (W1 + W2));

        then

        consider u,v be 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 be Element of V : u9 in ( Up W1) & v9 in ( Up W2) } by A7, A10;

        hence thesis by RUSUB_4:def 9;

      end;

      then ( Up (W1 + W2)) c= (( Up W1) + ( Up W2));

      hence thesis by A6, XBOOLE_0:def 10;

    end;

    

     Lm4: for V be RealLinearSpace, W1,W2 be Subspace of V holds ( Up (W1 /\ W2)) = (( Up W1) /\ ( Up W2))

    proof

      let V be RealLinearSpace;

      let W1,W2 be Subspace of V;

      

       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 be object st x in (( Up W1) /\ ( Up W2)) holds x in ( Up (W1 /\ W2))

      proof

        let x be object;

        assume

         A2: x in (( Up W1) /\ ( Up 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 thesis by A1, A3, XBOOLE_0:def 4;

      end;

      then

       A4: (( Up W1) /\ ( Up W2)) c= ( Up (W1 /\ W2));

      for x be object st x in ( Up (W1 /\ W2)) holds x in (( Up W1) /\ ( Up W2))

      proof

        let x be object;

        assume

         A5: x in ( Up (W1 /\ 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 thesis by A6, XBOOLE_0:def 4;

      end;

      then ( Up (W1 /\ W2)) c= (( Up W1) /\ ( Up W2));

      hence thesis by A4, XBOOLE_0:def 10;

    end;

    theorem :: CONVEX2:7

    for V be RealLinearSpace, M be Subset of V holds ( Convex-Family M) <> {} ;

    

     Lm5: for V be RealLinearSpace, L1,L2 be Convex_Combination of V, a,b be Real st (a * b) > 0 holds ( Carrier ((a * L1) + (b * L2))) = (( Carrier (a * L1)) \/ ( Carrier (b * L2)))

    proof

      let V be RealLinearSpace;

      let L1,L2 be Convex_Combination of V;

      let a,b be Real;

      assume (a * b) > 0 ;

      then

       A1: not (a >= 0 & b <= 0 or a <= 0 & b >= 0 );

      then

       A2: ( Carrier L2) = ( Carrier (b * L2)) by RLVECT_2: 42;

      

       A3: ( Carrier L1) = ( Carrier (a * L1)) by A1, RLVECT_2: 42;

      for x be object st x in (( Carrier (a * L1)) \/ ( Carrier (b * L2))) holds x in ( Carrier ((a * L1) + (b * L2)))

      proof

        let x be object;

        assume

         A4: x in (( Carrier (a * L1)) \/ ( Carrier (b * L2)));

        now

          per cases by A4, XBOOLE_0:def 3;

            suppose

             A5: x in ( Carrier (a * L1));

            then x in { v where v be Element of V : ((a * L1) . v) <> 0 } by RLVECT_2:def 4;

            then

            consider v be 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

                per cases ;

                  suppose

                   A9: v in ( Carrier L2);

                  then

                   A10: (L2 . v) > 0 by CONVEX1: 22;

                  now

                    per cases by A1;

                      suppose

                       A11: a > 0 & b > 0 ;

                      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 thesis by RLVECT_2: 19;

                    end;

                      suppose

                       A13: a < 0 & b < 0 ;

                      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 thesis by RLVECT_2: 19;

                    end;

                  end;

                  hence thesis;

                end;

                  suppose not v in ( Carrier 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 thesis by RLVECT_2: 19;

                end;

              end;

              hence thesis;

            end;

            hence thesis by A6;

          end;

            suppose

             A15: x in ( Carrier (b * L2));

            then x in { v where v be Element of V : ((b * L2) . v) <> 0 } by RLVECT_2:def 4;

            then

            consider v be 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

                per cases ;

                  suppose

                   A19: v in ( Carrier L1);

                  then

                   A20: (L1 . v) > 0 by CONVEX1: 22;

                  now

                    per cases by A1;

                      suppose

                       A21: a > 0 & b > 0 ;

                      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 thesis by RLVECT_2: 19;

                    end;

                      suppose

                       A23: a < 0 & b < 0 ;

                      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 thesis by RLVECT_2: 19;

                    end;

                  end;

                  hence thesis;

                end;

                  suppose not v in ( Carrier L1);

                  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 thesis by RLVECT_2: 19;

                end;

              end;

              hence thesis;

            end;

            hence thesis by A16;

          end;

        end;

        hence thesis;

      end;

      then

       A25: (( Carrier (a * L1)) \/ ( Carrier (b * L2))) c= ( Carrier ((a * L1) + (b * L2)));

      ( Carrier ((a * L1) + (b * L2))) c= (( Carrier (a * L1)) \/ ( Carrier (b * L2))) by RLVECT_2: 37;

      hence thesis by A25, XBOOLE_0:def 10;

    end;

    

     Lm6: for F,G be Function st (F,G) are_fiberwise_equipotent holds for x1,x2 be set st x1 in ( dom F) & x2 in ( dom F) & x1 <> x2 holds ex z1,z2 be 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;

      assume (F,G) are_fiberwise_equipotent ;

      then

      consider H be 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;

      assume that

       A5: x1 in ( dom F) and

       A6: x2 in ( dom F) and

       A7: x1 <> x2;

      

       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 thesis by A8, A9;

    end;

    

     Lm7: for V be RealLinearSpace, L be Linear_Combination of V, A be Subset of V st A c= ( Carrier L) holds ex L1 be Linear_Combination of V st ( Carrier L1) = A

    proof

      let V be RealLinearSpace;

      let L be Linear_Combination of V;

      let A be Subset of V;

      consider F be 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 P[ object, object] means ($1 in A implies $2 = (F . $1)) & ( not $1 in A implies $2 = 0 );

      

       A4: for x be object st x in the carrier of V holds ex y be object st P[x, y]

      proof

        let x be object;

        assume x in the carrier of V;

        now

          per cases ;

            suppose x in A;

            hence thesis;

          end;

            suppose not x in A;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      consider L1 be Function such that

       A5: ( dom L1) = the carrier of V & for x be object st x in the carrier of V holds P[x, (L1 . x)] from CLASSES1:sch 1( A4);

      for y be object st y in ( rng L1) holds y in REAL

      proof

        let y be object;

        assume y in ( rng L1);

        then

        consider x be object such that

         A6: x in ( dom L1) and

         A7: y = (L1 . x) by FUNCT_1:def 3;

        reconsider x as Element of V by A5, A6;

        now

          per cases ;

            suppose

             A8: x in A;

            

             A9: (F . x) in ( rng F) by A2, FUNCT_1: 3;

            y = (F . x) by A5, A7, A8;

            hence thesis by A3, A9;

          end;

            suppose not x in A;

            then (L1 . x) = ( In ( 0 , REAL )) by A5;

            hence thesis by A7;

          end;

        end;

        hence thesis;

      end;

      then ( rng L1) c= REAL ;

      then

       A10: L1 is Element of ( Funcs (the carrier of V, REAL )) by A5, FUNCT_2:def 2;

      assume

       A11: A c= ( Carrier L);

      then

      reconsider A as finite Subset of V by FINSET_1: 1;

      for v be Element of V st not v in A holds (L1 . v) = 0 by A5;

      then

      reconsider L1 as Linear_Combination of V by A10, RLVECT_2:def 3;

      for v be object st v in ( Carrier L1) holds v in A

      proof

        let v be object;

        assume

         A12: v in ( Carrier L1);

        then

        reconsider v as Element of V;

        (L1 . v) <> 0 by A12, RLVECT_2: 19;

        hence thesis by A5;

      end;

      then

       A13: ( Carrier L1) c= A;

      take L1;

      for v be object st v in A holds v in ( Carrier L1)

      proof

        let v be object;

        assume

         A14: v in A;

        then

        reconsider v as Element of V;

        (L1 . v) = (F . v) & (L . v) <> 0 by A11, A5, A14, RLVECT_2: 19;

        hence thesis by A1, RLVECT_2: 19;

      end;

      then A c= ( Carrier L1);

      hence thesis by A13, XBOOLE_0:def 10;

    end;

    theorem :: CONVEX2:8

    

     Th8: for V be RealLinearSpace, L1,L2 be Convex_Combination of V, r be Real st 0 < r & r < 1 holds ((r * L1) + ((1 - r) * L2)) is Convex_Combination of V

    proof

      let V be RealLinearSpace;

      let L1,L2 be Convex_Combination of V;

      let r be Real;

      assume that

       A1: 0 < r and

       A2: r < 1;

      

       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 be FinSequence of the carrier of V such that

       A4: F2 is one-to-one and

       A5: ( rng F2) = ( Carrier L2) and

       A6: ex f be FinSequence of REAL st ( len f) = ( len F2) & ( Sum f) = 1 & for n be Nat st n in ( dom f) holds (f . n) = (L2 . (F2 . n)) & (f . n) >= 0 by CONVEX1:def 3;

      set Btm = (( Carrier L) \ ( Carrier (r * L1)));

      set Top = (( Carrier L) \ ( Carrier ((1 - r) * L2)));

      consider F1 be FinSequence of the carrier of V such that

       A7: F1 is one-to-one and

       A8: ( rng F1) = ( Carrier L1) and

       A9: ex f be FinSequence of REAL st ( len f) = ( len F1) & ( Sum f) = 1 & for n be Nat st n in ( dom f) holds (f . n) = (L1 . (F1 . n)) & (f . n) >= 0 by CONVEX1:def 3;

      consider Lt be Linear_Combination of V such that

       A10: ( Carrier Lt) = Top 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 L) = (( Carrier (r * L1)) \/ ( Carrier ((1 - r) * L2))) by Lm5;

      then

      consider Lm be Linear_Combination of V such that

       A15: ( Carrier Lm) = Mid by Lm7, XBOOLE_1: 29;

      consider Lb be Linear_Combination of V such that

       A16: ( Carrier Lb) = Btm by Lm7, XBOOLE_1: 36;

      consider Ft be 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 be 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 be 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 be FinSequence of REAL such that

       A26: ( len f2) = ( len F2) and

       A27: ( Sum f2) = 1 and

       A28: for n be Nat st n in ( dom f2) holds (f2 . n) = (L2 . (F2 . n)) & (f2 . n) >= 0 by A6;

      deffunc F( set) = (L1 . (Ft . $1));

      consider ft be FinSequence such that

       A29: ( len ft) = ( len Ft) & for j be Nat st j in ( dom ft) holds (ft . j) = F(j) from FINSEQ_1:sch 2;

      ( rng ft) c= REAL

      proof

        let y be object;

        consider L1f be 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);

        then

        consider x be object such that

         A33: x in ( dom ft) and

         A34: (ft . x) = y by FUNCT_1:def 3;

        reconsider 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 thesis by A34, A32;

      end;

      then

      reconsider ft as FinSequence of REAL by FINSEQ_1:def 4;

      deffunc F( set) = (L1 . (Fm . $1));

      consider fm1 be FinSequence such that

       A37: ( len fm1) = ( len Fm) & for j be Nat st j in ( dom fm1) holds (fm1 . j) = F(j) from FINSEQ_1:sch 2;

      ( rng fm1) c= REAL

      proof

        let y be object;

        consider L1f be 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);

        then

        consider x be object such that

         A41: x in ( dom fm1) and

         A42: (fm1 . x) = y by FUNCT_1:def 3;

        reconsider 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 thesis by A42, A40;

      end;

      then

      reconsider fm1 as FinSequence of REAL by FINSEQ_1:def 4;

      deffunc F( set) = (L2 . (Fm . $1));

      consider fm2 be FinSequence such that

       A45: ( len fm2) = ( len Fm) & for j be Nat st j in ( dom fm2) holds (fm2 . j) = F(j) from FINSEQ_1:sch 2;

      

       A46: for x be object st x in ( dom (ft ^ fm1)) holds ((ft ^ fm1) . x) = (L1 . ((Ft ^ Fm) . x))

      proof

        let x be object;

        assume

         A47: x in ( dom (ft ^ fm1));

        then

        reconsider n = x as Element of NAT ;

        now

          per cases by A47, FINSEQ_1: 25;

            suppose

             A48: n in ( dom ft);

            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 thesis by A49, FINSEQ_1:def 7;

          end;

            suppose ex m be Nat st m in ( dom fm1) & n = (( len ft) + m);

            then

            consider m be 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 thesis by A29, A51, A52, FINSEQ_1:def 7;

          end;

        end;

        hence thesis;

      end;

      for x be object holds x in ( dom (ft ^ fm1)) iff x in ( dom (Ft ^ Fm)) & ((Ft ^ Fm) . x) in ( dom L1)

      proof

        let x be object;

        

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

          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 thesis by A55;

        end;

        hence thesis by A54;

      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 be object holds x in ( dom f2) iff x in ( dom F2) & (F2 . x) in ( dom L2)

      proof

        let x be object;

         A59:

        now

          assume x in ( dom f2);

          then x in ( Seg ( len F2)) by A26, FINSEQ_1:def 3;

          hence x in ( dom F2) by FINSEQ_1:def 3;

          then (F2 . x) in ( rng F2) by FUNCT_1: 3;

          hence (F2 . x) in ( dom L2) by A5, A57;

        end;

        now

          assume that

           A60: x in ( dom F2) and (F2 . x) in ( dom L2);

          x in ( Seg ( len F2)) by A60, FINSEQ_1:def 3;

          hence x in ( dom f2) by A26, FINSEQ_1:def 3;

        end;

        hence thesis by A59;

      end;

      deffunc F( set) = (L2 . (Fb . $1));

      consider fb be FinSequence such that

       A61: ( len fb) = ( len Fb) & for j be Nat st j in ( dom fb) holds (fb . j) = F(j) from FINSEQ_1:sch 2;

      ( rng fm2) c= REAL

      proof

        let y be object;

        consider L2f be 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);

        then

        consider x be object such that

         A65: x in ( dom fm2) and

         A66: (fm2 . x) = y by FUNCT_1:def 3;

        reconsider 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 thesis by A66, A64;

      end;

      then

      reconsider 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 object;

        consider L2f be 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);

        then

        consider x be object such that

         A73: x in ( dom fb) and

         A74: (fb . x) = y by FUNCT_1:def 3;

        reconsider 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 thesis by A74, A72;

      end;

      then

      reconsider fb as FinSequence of REAL by FINSEQ_1:def 4;

      set f = (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb));

      consider f1 be FinSequence of REAL such that

       A77: ( len f1) = ( len F1) and

       A78: ( Sum f1) = 1 and

       A79: for n be Nat st n in ( dom f1) holds (f1 . n) = (L1 . (F1 . n)) & (f1 . n) >= 0 by A9;

      ( len f) = (( 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 f) = ( len F) by FINSEQ_1: 22;

      

       A81: ( dom L1) = the carrier of V by FUNCT_2: 92;

      

       A82: for x be object holds x in ( dom f1) iff x in ( dom F1) & (F1 . x) in ( dom L1)

      proof

        let x be object;

         A83:

        now

          assume x in ( dom f1);

          then x in ( Seg ( len F1)) by A77, FINSEQ_1:def 3;

          hence x in ( dom F1) by FINSEQ_1:def 3;

          then (F1 . x) in ( rng F1) by FUNCT_1: 3;

          hence (F1 . x) in ( dom L1) by A8, A81;

        end;

        now

          assume that

           A84: x in ( dom F1) and (F1 . x) in ( dom L1);

          x in ( Seg ( len F1)) by A84, FINSEQ_1:def 3;

          hence x in ( dom f1) by A77, FINSEQ_1:def 3;

        end;

        hence thesis by A83;

      end;

      

       A85: ( rng (Ft ^ Fm)) = (( Carrier Lt) \/ ( Carrier Lm)) by A18, A22, FINSEQ_1: 31;

      for x be object 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 be object 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 L) \ ( 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 be Element of NAT st n in ( dom f) holds (f . n) = (L . (F . n)) & (f . n) >= 0

      proof

        let n be Element of NAT ;

        assume

         A92: n in ( dom f);

        now

          per cases by A92, FINSEQ_1: 25;

            suppose

             A93: n in ( dom ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))));

            then

             A94: (f . n) = (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) . n) by FINSEQ_1:def 7;

            now

              per cases by A93, FINSEQ_1: 25;

                suppose

                 A95: n in ( dom (r * ft));

                ( 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) = (F . 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: (f . 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 (f . 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 (f . n) = (L . (F . n)) by A98, A96, FINSEQ_1:def 7;

                

                 A101: ( rng Ft) c= ( rng (Ft ^ Fm)) by FINSEQ_1: 29;

                (Ft . n) in ( rng Ft) by A98, FUNCT_1: 3;

                then

                consider m9 be object such that

                 A102: m9 in ( dom F1) and

                 A103: (F1 . m9) = (Ft . n) by A23, A101, FUNCT_1:def 3;

                reconsider 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 (f . n) >= 0 by A1, A100, A103;

              end;

                suppose ex k be Nat st k in ( dom ((r * fm1) + ((1 - r) * fm2))) & n = (( len (r * ft)) + k);

                then

                consider m be 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: (f . 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) = (F . 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 (f . n) = (((r * L1) + ((1 - r) * L2)) . (Fm . m)) by A111, RLVECT_2:def 10;

                hence (f . n) = (L . (F . n)) by A105, A107, A112, A113, FINSEQ_1:def 7;

                ( rng Fm) c= ( rng (Ft ^ Fm)) by FINSEQ_1: 30;

                then

                consider m9 be object such that

                 A114: m9 in ( dom F1) and

                 A115: (F1 . m9) = (Fm . m) by A23, A108, FUNCT_1:def 3;

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

                ( rng Fm) c= ( rng (Fm ^ Fb)) by FINSEQ_1: 29;

                then

                consider m9 be object such that

                 A117: m9 in ( dom F2) and

                 A118: (F2 . m9) = (Fm . m) by A91, A108, FUNCT_1:def 3;

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

                then ((r * (L1 . (Fm . m))) + ((1 - r) * (L2 . (Fm . m)))) >= ( 0 + 0 qua Nat) by A116;

                hence (f . n) >= 0 by A111;

              end;

            end;

            hence thesis;

          end;

            suppose ex m be Nat st m in ( dom ((1 - r) * fb)) & n = (( len ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2)))) + m);

            then

            consider m be 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: (f . 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 (f . 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 (f . n) = (L . (F . n)) by A120, A122, A125, FINSEQ_1:def 7;

            ( rng Fb) c= ( rng (Fm ^ Fb)) by FINSEQ_1: 30;

            then

            consider m9 be object such that

             A126: m9 in ( dom F2) and

             A127: (F2 . m9) = (Fb . m) by A91, A123, FUNCT_1:def 3;

            reconsider 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 (f . n) >= 0 by A11, A124, A127;

          end;

        end;

        hence thesis;

      end;

      then

       A128: for n be Nat st n in ( dom f) holds (f . n) = (L . (F . n)) & (f . n) >= 0 ;

      

       A129: ( rng Fb) = (( Carrier L) \ ( Carrier L1)) by A1, A16, A20, RLVECT_2: 42;

      then ( rng (Ft ^ Fm)) misses ( rng Fb) by A8, A23, XBOOLE_1: 79;

      then

       A130: F is one-to-one by A19, A25, FINSEQ_3: 91;

      

       A131: for x be object st x in ( dom (fm2 ^ fb)) holds ((fm2 ^ fb) . x) = (L2 . ((Fm ^ Fb) . x))

      proof

        let x be object;

        assume

         A132: x in ( dom (fm2 ^ fb));

        then

        reconsider n = x as Element of NAT ;

        now

          per cases by A132, FINSEQ_1: 25;

            suppose

             A133: n in ( dom fm2);

            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 thesis by A134, FINSEQ_1:def 7;

          end;

            suppose ex m be Nat st m in ( dom fb) & n = (( len fm2) + m);

            then

            consider m be 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 thesis by A45, A136, A137, FINSEQ_1:def 7;

          end;

        end;

        hence thesis;

      end;

      for x be object holds x in ( dom (fm2 ^ fb)) iff x in ( dom (Fm ^ Fb)) & ((Fm ^ Fb) . x) in ( dom L2)

      proof

        let x be object;

        

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

          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 thesis by A140;

        end;

        hence thesis by A139;

      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 f) = (( 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 F) = (( Carrier L1) \/ (( Carrier L) \ ( Carrier L1))) by A8, A23, A129, FINSEQ_1: 31

      .= (( Carrier L1) \/ ( Carrier L)) by XBOOLE_1: 39

      .= ( Carrier L) by A3, A14, XBOOLE_1: 7, XBOOLE_1: 12;

      hence thesis by A130, A144, A80, A128, CONVEX1:def 3;

    end;

    theorem :: CONVEX2:9

    for V be RealLinearSpace, M be non empty Subset of V, L1,L2 be Convex_Combination of M, r be Real st 0 < r & r < 1 holds ((r * L1) + ((1 - r) * L2)) is Convex_Combination of M

    proof

      let V be RealLinearSpace;

      let M be non empty Subset of V;

      let L1,L2 be Convex_Combination of M;

      let r be Real;

      

       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;

      hence thesis by A1, Th8, RLVECT_2: 38;

    end;

    begin

    theorem :: CONVEX2:10

    for V be RealLinearSpace, W1,W2 be Subspace of V holds ( Up (W1 + W2)) = (( Up W1) + ( Up W2)) by Lm3;

    theorem :: CONVEX2:11

    for V be RealLinearSpace, W1,W2 be Subspace of V holds ( Up (W1 /\ W2)) = (( Up W1) /\ ( Up W2)) by Lm4;

    theorem :: CONVEX2:12

    for V be RealLinearSpace, L1,L2 be Convex_Combination of V, a,b be 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 be Function st (F,G) are_fiberwise_equipotent holds for x1,x2 be set st x1 in ( dom F) & x2 in ( dom F) & x1 <> x2 holds ex z1,z2 be 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 be RealLinearSpace, L be Linear_Combination of V, A be Subset of V st A c= ( Carrier L) holds ex L1 be Linear_Combination of V st ( Carrier L1) = A by Lm7;