convex3.miz



    begin

    definition

      let V be RealLinearSpace;

      defpred P[ object] means $1 is Convex_Combination of V;

      :: CONVEX3:def1

      func ConvexComb (V) -> set means

      : Def1: for L be object holds L in it iff L is Convex_Combination of V;

      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 Convex_Combination of V by A1;

        assume L is Convex_Combination of V;

        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

    definition

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

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

      :: CONVEX3:def2

      func ConvexComb (M) -> set means for L be object holds L in it iff L is Convex_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 Convex_Combination of M by A1;

        assume L is Convex_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

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

    theorem :: CONVEX3:1

    

     Th1: for V be RealLinearSpace, v be VECTOR of V holds ex L be Convex_Combination of V st ( Sum L) = v & for A be non empty Subset of V st v in A holds L is Convex_Combination of A

    proof

      let V be RealLinearSpace;

      let v be VECTOR of V;

      consider L be Linear_Combination of {v} such that

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

      consider F be FinSequence of the carrier of V such that

       A2: F is one-to-one & ( rng F) = ( Carrier L) and ( Sum L) = ( Sum (L (#) F)) by RLVECT_2:def 8;

      v in ( Carrier L) by A1, RLVECT_2: 19;

      then ( Carrier L) c= {v} & {v} c= ( Carrier L) by RLVECT_2:def 6, ZFMISC_1: 31;

      then

       A3: {v} = ( Carrier L) by XBOOLE_0:def 10;

      then F = <*v*> by A2, FINSEQ_3: 97;

      then

       A4: (F . 1) = v by FINSEQ_1:def 8;

      deffunc F( set) = (L . (F . $1));

      consider f be FinSequence such that

       A5: ( len f) = ( len F) & for n be Nat st n in ( dom f) holds (f . n) = F(n) from FINSEQ_1:sch 2;

      

       A6: 1 in REAL by XREAL_0:def 1;

      

       A7: ( len F) = 1 by A3, A2, FINSEQ_3: 96;

      then 1 in ( dom f) by A5, FINSEQ_3: 25;

      then

       A8: (f . 1) = (L . (F . 1)) by A5;

      then f = <*1*> by A1, A5, A7, A4, FINSEQ_1: 40;

      then ( rng f) = {1} by FINSEQ_1: 38;

      then ( rng f) c= REAL by ZFMISC_1: 31, A6;

      then

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

      

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

      proof

        let n be Nat;

        assume

         A10: n in ( dom f);

        then n in ( Seg ( len f)) by FINSEQ_1:def 3;

        hence thesis by A1, A5, A7, A8, A4, A10, FINSEQ_1: 2, TARSKI:def 1;

      end;

      f = <*1*> by A1, A5, A7, A8, A4, FINSEQ_1: 40;

      then ( Sum f) = jj by FINSOP_1: 11;

      then

      reconsider L as Convex_Combination of V by A2, A5, A9, CONVEX1:def 3;

      

       A11: for A be non empty Subset of V st v in A holds L is Convex_Combination of A by A3, RLVECT_2:def 6, ZFMISC_1: 31;

      take L;

      ( Sum L) = (1 * v) by A1, A3, RLVECT_2: 35;

      hence thesis by A11, RLVECT_1:def 8;

    end;

    reconsider jd = (1 / 2), jt = (1 / 3) as Element of REAL by XREAL_0:def 1;

    theorem :: CONVEX3:2

    for V be RealLinearSpace, v1,v2 be VECTOR of V st v1 <> v2 holds ex L be Convex_Combination of V st for A be non empty Subset of V st {v1, v2} c= A holds L is Convex_Combination of A

    proof

      let V be RealLinearSpace;

      let v1,v2 be VECTOR of V;

      assume

       A1: v1 <> v2;

      consider L be Linear_Combination of {v1, v2} such that

       A2: (L . v1) = (jj / 2) & (L . v2) = (jj / 2) by A1, RLVECT_4: 38;

      consider F be FinSequence of the carrier of V such that

       A3: F is one-to-one & ( rng F) = ( Carrier L) and ( Sum L) = ( Sum (L (#) F)) by RLVECT_2:def 8;

      deffunc F( set) = (L . (F . $1));

      consider f be FinSequence such that

       A4: ( len f) = ( len F) & for n be Nat st n in ( dom f) holds (f . n) = F(n) from FINSEQ_1:sch 2;

      v1 in ( Carrier L) & v2 in ( Carrier L) by A2, RLVECT_2: 19;

      then ( Carrier L) c= {v1, v2} & {v1, v2} c= ( Carrier L) by RLVECT_2:def 6, ZFMISC_1: 32;

      then

       A5: {v1, v2} = ( Carrier L) by XBOOLE_0:def 10;

      then

       A6: ( len F) = 2 by A1, A3, FINSEQ_3: 98;

      then 2 in ( dom f) by A4, FINSEQ_3: 25;

      then

       A7: (f . 2) = (L . (F . 2)) by A4;

      1 in ( dom f) by A4, A6, FINSEQ_3: 25;

      then

       A8: (f . 1) = (L . (F . 1)) by A4;

      now

        per cases by A1, A5, A3, FINSEQ_3: 99;

          suppose F = <*v1, v2*>;

          then

           A9: (F . 1) = v1 & (F . 2) = v2 by FINSEQ_1: 44;

          then f = <*(1 / 2), (1 / 2)*> by A2, A4, A6, A8, A7, FINSEQ_1: 44;

          then f = ( <*jd*> ^ <*jd*>) by FINSEQ_1:def 9;

          

          then ( rng f) = (( rng <*(1 / 2)*>) \/ ( rng <*jd*>)) by FINSEQ_1: 31

          .= {jd} by FINSEQ_1: 38;

          then

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

          

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

          proof

            let n be Nat;

            assume

             A11: n in ( dom f);

            then n in ( Seg ( len f)) by FINSEQ_1:def 3;

            hence thesis by A2, A4, A6, A8, A7, A9, A11, FINSEQ_1: 2, TARSKI:def 2;

          end;

          f = <*(1 / 2), (1 / 2)*> by A2, A4, A6, A8, A7, A9, FINSEQ_1: 44;

          

          then ( Sum f) = ((1 / 2) + (1 / 2)) by RVSUM_1: 77

          .= 1;

          then

          reconsider L as Convex_Combination of V by A3, A4, A10, CONVEX1:def 3;

          take L;

          for A be non empty Subset of V st {v1, v2} c= A holds L is Convex_Combination of A by A5, RLVECT_2:def 6;

          hence thesis;

        end;

          suppose F = <*v2, v1*>;

          then

           A12: (F . 1) = v2 & (F . 2) = v1 by FINSEQ_1: 44;

          then f = <*(1 / 2), (1 / 2)*> by A2, A4, A6, A8, A7, FINSEQ_1: 44;

          then f = ( <*jd*> ^ <*jd*>) by FINSEQ_1:def 9;

          

          then ( rng f) = (( rng <*(1 / 2)*>) \/ ( rng <*jd*>)) by FINSEQ_1: 31

          .= {jd} by FINSEQ_1: 38;

          then

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

          

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

          proof

            let n be Nat;

            assume

             A14: n in ( dom f);

            then n in ( Seg ( len f)) by FINSEQ_1:def 3;

            hence thesis by A2, A4, A6, A8, A7, A12, A14, FINSEQ_1: 2, TARSKI:def 2;

          end;

          f = <*(1 / 2), (1 / 2)*> by A2, A4, A6, A8, A7, A12, FINSEQ_1: 44;

          

          then ( Sum f) = ((1 / 2) + (1 / 2)) by RVSUM_1: 77

          .= 1;

          then

          reconsider L as Convex_Combination of V by A3, A4, A13, CONVEX1:def 3;

          take L;

          for A be non empty Subset of V st {v1, v2} c= A holds L is Convex_Combination of A by A5, RLVECT_2:def 6;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: CONVEX3:3

    for V be RealLinearSpace, v1,v2,v3 be VECTOR of V st v1 <> v2 & v1 <> v3 & v2 <> v3 holds ex L be Convex_Combination of V st for A be non empty Subset of V st {v1, v2, v3} c= A holds L is Convex_Combination of A

    proof

      let V be RealLinearSpace;

      let v1,v2,v3 be VECTOR of V;

      assume that

       A1: v1 <> v2 and

       A2: v1 <> v3 and

       A3: v2 <> v3;

      consider L be Linear_Combination of {v1, v2, v3} such that

       A4: (L . v1) = (jj / 3) & (L . v2) = (jj / 3) & (L . v3) = (jj / 3) by A1, A2, A3, RLVECT_4: 39;

      consider F be FinSequence of the carrier of V such that

       A5: F is one-to-one & ( rng F) = ( Carrier L) and ( Sum L) = ( Sum (L (#) F)) by RLVECT_2:def 8;

      deffunc F( set) = (L . (F . $1));

      consider f be FinSequence such that

       A6: ( len f) = ( len F) & for n be Nat st n in ( dom f) holds (f . n) = F(n) from FINSEQ_1:sch 2;

      for x be object st x in {v1, v2, v3} holds x in ( Carrier L)

      proof

        let x be object;

        assume

         A7: x in {v1, v2, v3};

        then

        reconsider x as VECTOR of V;

        x = v1 or x = v2 or x = v3 by A7, ENUMSET1:def 1;

        hence thesis by A4, RLVECT_2: 19;

      end;

      then ( Carrier L) c= {v1, v2, v3} & {v1, v2, v3} c= ( Carrier L) by RLVECT_2:def 6;

      then

       A8: {v1, v2, v3} = ( Carrier L) by XBOOLE_0:def 10;

      then

       A9: ( len F) = 3 by A1, A2, A3, A5, FINSEQ_3: 101;

      then 2 in ( dom f) by A6, FINSEQ_3: 25;

      then

       A10: (f . 2) = (L . (F . 2)) by A6;

      3 in ( dom f) by A6, A9, FINSEQ_3: 25;

      then

       A11: (f . 3) = (L . (F . 3)) by A6;

      1 in ( dom f) by A6, A9, FINSEQ_3: 25;

      then

       A12: (f . 1) = (L . (F . 1)) by A6;

      now

        per cases by A1, A2, A3, A8, A5, CONVEX1: 31;

          suppose

           A13: F = <*v1, v2, v3*>;

          then

           A14: (F . 3) = v3 by FINSEQ_1: 45;

          

           A15: (F . 1) = v1 & (F . 2) = v2 by A13, FINSEQ_1: 45;

          then f = <*(1 / 3), (1 / 3), (1 / 3)*> by A4, A6, A9, A12, A10, A11, A14, FINSEQ_1: 45;

          then f = (( <*jt*> ^ <*jt*>) ^ <*jt*>) by FINSEQ_1:def 10;

          

          then ( rng f) = (( rng ( <*jt*> ^ <*jt*>)) \/ ( rng <*(1 / 3)*>)) by FINSEQ_1: 31

          .= ((( rng <*(1 / 3)*>) \/ ( rng <*jt*>)) \/ ( rng <*jt*>)) by FINSEQ_1: 31

          .= {jt} by FINSEQ_1: 38;

          then

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

          

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

          proof

            let n be Nat;

            assume

             A17: n in ( dom f);

            then n in ( Seg ( len f)) by FINSEQ_1:def 3;

            hence thesis by A4, A6, A9, A12, A10, A11, A15, A14, A17, ENUMSET1:def 1, FINSEQ_3: 1;

          end;

          f = <*(1 / 3), (1 / 3), (1 / 3)*> by A4, A6, A9, A12, A10, A11, A15, A14, FINSEQ_1: 45;

          

          then ( Sum f) = (((1 / 3) + (1 / 3)) + (1 / 3)) by RVSUM_1: 78

          .= 1;

          then

          reconsider L as Convex_Combination of V by A5, A6, A16, CONVEX1:def 3;

          take L;

          for A be non empty Subset of V st {v1, v2, v3} c= A holds L is Convex_Combination of A by A8, RLVECT_2:def 6;

          hence thesis;

        end;

          suppose

           A18: F = <*v1, v3, v2*>;

          then

           A19: (F . 3) = v2 by FINSEQ_1: 45;

          

           A20: (F . 1) = v1 & (F . 2) = v3 by A18, FINSEQ_1: 45;

          then f = <*(1 / 3), (1 / 3), (1 / 3)*> by A4, A6, A9, A12, A10, A11, A19, FINSEQ_1: 45;

          then f = (( <*jt*> ^ <*jt*>) ^ <*jt*>) by FINSEQ_1:def 10;

          

          then ( rng f) = (( rng ( <*jt*> ^ <*jt*>)) \/ ( rng <*jt*>)) by FINSEQ_1: 31

          .= ((( rng <*jt*>) \/ ( rng <*jt*>)) \/ ( rng <*jt*>)) by FINSEQ_1: 31

          .= {jt} by FINSEQ_1: 38;

          then

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

          

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

          proof

            let n be Nat;

            assume

             A22: n in ( dom f);

            then n in ( Seg ( len f)) by FINSEQ_1:def 3;

            hence thesis by A4, A6, A9, A12, A10, A11, A20, A19, A22, ENUMSET1:def 1, FINSEQ_3: 1;

          end;

          f = <*(1 / 3), (1 / 3), (1 / 3)*> by A4, A6, A9, A12, A10, A11, A20, A19, FINSEQ_1: 45;

          

          then ( Sum f) = (((1 / 3) + (1 / 3)) + (1 / 3)) by RVSUM_1: 78

          .= 1;

          then

          reconsider L as Convex_Combination of V by A5, A6, A21, CONVEX1:def 3;

          take L;

          for A be non empty Subset of V st {v1, v2, v3} c= A holds L is Convex_Combination of A by A8, RLVECT_2:def 6;

          hence thesis;

        end;

          suppose

           A23: F = <*v2, v1, v3*>;

          then

           A24: (F . 3) = v3 by FINSEQ_1: 45;

          

           A25: (F . 1) = v2 & (F . 2) = v1 by A23, FINSEQ_1: 45;

          then f = <*(1 / 3), (1 / 3), (1 / 3)*> by A4, A6, A9, A12, A10, A11, A24, FINSEQ_1: 45;

          then f = (( <*jt*> ^ <*jt*>) ^ <*jt*>) by FINSEQ_1:def 10;

          

          then ( rng f) = (( rng ( <*jt*> ^ <*jt*>)) \/ ( rng <*jt*>)) by FINSEQ_1: 31

          .= ((( rng <*jt*>) \/ ( rng <*jt*>)) \/ ( rng <*jt*>)) by FINSEQ_1: 31

          .= {jt} by FINSEQ_1: 38;

          then

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

          

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

          proof

            let n be Nat;

            assume

             A27: n in ( dom f);

            then n in ( Seg ( len f)) by FINSEQ_1:def 3;

            hence thesis by A4, A6, A9, A12, A10, A11, A25, A24, A27, ENUMSET1:def 1, FINSEQ_3: 1;

          end;

          f = <*(1 / 3), (1 / 3), (1 / 3)*> by A4, A6, A9, A12, A10, A11, A25, A24, FINSEQ_1: 45;

          

          then ( Sum f) = (((1 / 3) + (1 / 3)) + (1 / 3)) by RVSUM_1: 78

          .= 1;

          then

          reconsider L as Convex_Combination of V by A5, A6, A26, CONVEX1:def 3;

          take L;

          for A be non empty Subset of V st {v1, v2, v3} c= A holds L is Convex_Combination of A by A8, RLVECT_2:def 6;

          hence thesis;

        end;

          suppose

           A28: F = <*v2, v3, v1*>;

          then

           A29: (F . 3) = v1 by FINSEQ_1: 45;

          

           A30: (F . 1) = v2 & (F . 2) = v3 by A28, FINSEQ_1: 45;

          then f = <*(1 / 3), (1 / 3), (1 / 3)*> by A4, A6, A9, A12, A10, A11, A29, FINSEQ_1: 45;

          then f = (( <*jt*> ^ <*jt*>) ^ <*jt*>) by FINSEQ_1:def 10;

          

          then ( rng f) = (( rng ( <*jt*> ^ <*jt*>)) \/ ( rng <*jt*>)) by FINSEQ_1: 31

          .= ((( rng <*jt*>) \/ ( rng <*jt*>)) \/ ( rng <*jt*>)) by FINSEQ_1: 31

          .= {jt} by FINSEQ_1: 38;

          then

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

          

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

          proof

            let n be Nat;

            assume

             A32: n in ( dom f);

            then n in ( Seg ( len f)) by FINSEQ_1:def 3;

            hence thesis by A4, A6, A9, A12, A10, A11, A30, A29, A32, ENUMSET1:def 1, FINSEQ_3: 1;

          end;

          f = <*(1 / 3), (1 / 3), (1 / 3)*> by A4, A6, A9, A12, A10, A11, A30, A29, FINSEQ_1: 45;

          

          then ( Sum f) = (((1 / 3) + (1 / 3)) + (1 / 3)) by RVSUM_1: 78

          .= 1;

          then

          reconsider L as Convex_Combination of V by A5, A6, A31, CONVEX1:def 3;

          take L;

          for A be non empty Subset of V st {v1, v2, v3} c= A holds L is Convex_Combination of A by A8, RLVECT_2:def 6;

          hence thesis;

        end;

          suppose

           A33: F = <*v3, v1, v2*>;

          then

           A34: (F . 3) = v2 by FINSEQ_1: 45;

          

           A35: (F . 1) = v3 & (F . 2) = v1 by A33, FINSEQ_1: 45;

          then f = <*(1 / 3), (1 / 3), (1 / 3)*> by A4, A6, A9, A12, A10, A11, A34, FINSEQ_1: 45;

          then f = (( <*jt*> ^ <*jt*>) ^ <*jt*>) by FINSEQ_1:def 10;

          

          then ( rng f) = (( rng ( <*jt*> ^ <*jt*>)) \/ ( rng <*jt*>)) by FINSEQ_1: 31

          .= ((( rng <*jt*>) \/ ( rng <*jt*>)) \/ ( rng <*jt*>)) by FINSEQ_1: 31

          .= {jt} by FINSEQ_1: 38;

          then

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

          

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

          proof

            let n be Nat;

            assume

             A37: n in ( dom f);

            then n in ( Seg ( len f)) by FINSEQ_1:def 3;

            hence thesis by A4, A6, A9, A12, A10, A11, A35, A34, A37, ENUMSET1:def 1, FINSEQ_3: 1;

          end;

          f = <*(1 / 3), (1 / 3), (1 / 3)*> by A4, A6, A9, A12, A10, A11, A35, A34, FINSEQ_1: 45;

          

          then ( Sum f) = (((1 / 3) + (1 / 3)) + (1 / 3)) by RVSUM_1: 78

          .= 1;

          then

          reconsider L as Convex_Combination of V by A5, A6, A36, CONVEX1:def 3;

          take L;

          for A be non empty Subset of V st {v1, v2, v3} c= A holds L is Convex_Combination of A by A8, RLVECT_2:def 6;

          hence thesis;

        end;

          suppose

           A38: F = <*v3, v2, v1*>;

          then

           A39: (F . 3) = v1 by FINSEQ_1: 45;

          

           A40: (F . 1) = v3 & (F . 2) = v2 by A38, FINSEQ_1: 45;

          then f = <*(1 / 3), (1 / 3), (1 / 3)*> by A4, A6, A9, A12, A10, A11, A39, FINSEQ_1: 45;

          then f = (( <*jt*> ^ <*jt*>) ^ <*jt*>) by FINSEQ_1:def 10;

          

          then ( rng f) = (( rng ( <*jt*> ^ <*jt*>)) \/ ( rng <*jt*>)) by FINSEQ_1: 31

          .= ((( rng <*jt*>) \/ ( rng <*jt*>)) \/ ( rng <*jt*>)) by FINSEQ_1: 31

          .= {jt} by FINSEQ_1: 38;

          then

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

          

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

          proof

            let n be Nat;

            assume

             A42: n in ( dom f);

            then n in ( Seg ( len f)) by FINSEQ_1:def 3;

            hence thesis by A4, A6, A9, A12, A10, A11, A40, A39, A42, ENUMSET1:def 1, FINSEQ_3: 1;

          end;

          f = <*(1 / 3), (1 / 3), (1 / 3)*> by A4, A6, A9, A12, A10, A11, A40, A39, FINSEQ_1: 45;

          

          then ( Sum f) = (((1 / 3) + (1 / 3)) + (1 / 3)) by RVSUM_1: 78

          .= 1;

          then

          reconsider L as Convex_Combination of V by A5, A6, A41, CONVEX1:def 3;

          take L;

          for A be non empty Subset of V st {v1, v2, v3} c= A holds L is Convex_Combination of A by A8, RLVECT_2:def 6;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    

     Lm1: for V be RealLinearSpace, M be non empty Subset of V st { ( Sum L) where L be Convex_Combination of M : L in ( ConvexComb V) } c= M holds M is convex

    proof

      let V be RealLinearSpace;

      let M be non empty Subset of V;

      assume

       A1: { ( Sum L) where L be Convex_Combination of M : L in ( ConvexComb V) } c= M;

      for u,v be VECTOR of V, r be Real st 0 < r & r < 1 & u in M & v in M holds ((r * u) + ((1 - r) * v)) in M

      proof

        set S = { ( Sum L) where L be Convex_Combination of M : L in ( ConvexComb V) };

        let u,v be VECTOR of V;

        let r be Real;

        assume that

         A2: 0 < r & r < 1 and

         A3: u in M and

         A4: v in M;

        consider Lv be Convex_Combination of V such that

         A5: ( Sum Lv) = v and

         A6: for A be non empty Subset of V st v in A holds Lv is Convex_Combination of A by Th1;

        reconsider Lv as Convex_Combination of M by A4, A6;

        consider Lu be Convex_Combination of V such that

         A7: ( Sum Lu) = u and

         A8: for A be non empty Subset of V st u in A holds Lu is Convex_Combination of A by Th1;

        reconsider Lu as Convex_Combination of M by A3, A8;

        

         A9: ((r * u) + ((1 - r) * v)) = (( Sum (r * Lu)) + ((1 - r) * ( Sum Lv))) by A7, A5, RLVECT_3: 2

        .= (( Sum (r * Lu)) + ( Sum ((1 - r) * Lv))) by RLVECT_3: 2

        .= ( Sum ((r * Lu) + ((1 - r) * Lv))) by RLVECT_3: 1;

        reconsider r as Real;

        

         A10: ((r * Lu) + ((1 - r) * Lv)) is Convex_Combination of M by A2, CONVEX2: 9;

        then ((r * Lu) + ((1 - r) * Lv)) in ( ConvexComb V) by Def1;

        then ((r * u) + ((1 - r) * v)) in S by A9, A10;

        hence thesis by A1;

      end;

      hence thesis by CONVEX1:def 2;

    end;

    

     Lm2: for V be RealLinearSpace, M be non empty Subset of V, L be Convex_Combination of M st ( card ( Carrier L)) >= 2 holds ex L1,L2 be Convex_Combination of M, r be Real st 0 < r & r < 1 & L = ((r * L1) + ((1 - r) * L2)) & ( card ( Carrier L1)) = 1 & ( card ( Carrier L2)) = (( card ( Carrier L)) - 1)

    proof

      let V be RealLinearSpace;

      let M be non empty Subset of V;

      let L be Convex_Combination of M;

      consider F be FinSequence of the carrier of V such that

       A1: F is one-to-one and

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

       A3: 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 CONVEX1:def 3;

      

       A4: for n,m be Nat st 1 <= n & n < m & m <= ( len F) holds (F . n) <> (F . m)

      proof

        let n,m be Nat;

        assume that

         A5: 1 <= n and

         A6: n < m and

         A7: m <= ( len F);

        n <= ( len F) by A6, A7, XXREAL_0: 2;

        then n in ( Seg ( len F)) by A5, FINSEQ_1: 1;

        then

         A8: n in ( dom F) by FINSEQ_1:def 3;

        1 <= m by A5, A6, XXREAL_0: 2;

        then m in ( Seg ( len F)) by A7, FINSEQ_1: 1;

        then

         A9: m in ( dom F) by FINSEQ_1:def 3;

        assume (F . n) = (F . m);

        hence contradiction by A1, A6, A8, A9, FUNCT_1:def 4;

      end;

      assume

       A10: ( card ( Carrier L)) >= 2;

      then

       A11: ( len F) >= 2 by A2, A4, GRAPH_5: 7;

      then

      consider i be Nat such that

       A12: ( len F) = (i + 1) by NAT_1: 6;

      set v = (F . ( len F));

      

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

      1 <= ( len F) by A11, XXREAL_0: 2;

      then

       A14: ( len F) in ( dom F) by FINSEQ_3: 25;

      then

       A15: (F . ( len F)) in ( rng F) by FUNCT_1: 3;

      ( rng F) c= the carrier of V by FINSEQ_1:def 4;

      then

      reconsider v as VECTOR of V by A15;

      

       A16: (F . ( len F)) in ( rng F) by A14, FUNCT_1: 3;

      reconsider i as Element of NAT by ORDINAL1:def 12;

      consider f be FinSequence of REAL such that

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

       A18: ( Sum f) = 1 and

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

      1 <= ( len f) by A17, A11, XXREAL_0: 2;

      then

       A20: 1 in ( Seg ( len f)) by FINSEQ_1: 1;

      then

       A21: 1 in ( dom f) by FINSEQ_1:def 3;

      1 in ( dom F) by A17, A20, FINSEQ_1:def 3;

      then (F . 1) in ( rng F) by FUNCT_1: 3;

      then

       A22: (L . (F . 1)) <> 0 by A2, RLVECT_2: 19;

      

       A23: for k be Nat st k in ( dom (f | i)) holds 0 <= ((f | i) . k)

      proof

        

         A24: ( dom (f | i)) c= ( dom f) by FINSEQ_5: 18;

        let k be Nat;

        assume

         A25: k in ( dom (f | i));

        (f | i) = (f | ( Seg i)) by FINSEQ_1:def 15;

        then ((f | i) . k) = (f . k) by A25, FUNCT_1: 47;

        hence thesis by A19, A25, A24;

      end;

      ( len F) >= (1 + 1) by A10, A2, A4, GRAPH_5: 7;

      then (( len F) - 1) >= 1 by XREAL_1: 19;

      then 1 in ( Seg i) by A12, FINSEQ_1: 1;

      then

       A26: 1 in ( dom (f | ( Seg i))) by A21, RELAT_1: 57;

      (f | i) = (f | ( Seg i)) by FINSEQ_1:def 15;

      

      then

       A27: ((f | i) . 1) = (f . 1) by A26, FUNCT_1: 47

      .= (L . (F . 1)) by A19, A21;

      

       A28: 1 in ( dom (f | i)) by A26, FINSEQ_1:def 15;

      then ((f | i) . 1) >= 0 by A23;

      then

       A29: ( Sum (f | i)) > 0 by A23, A28, A27, A22, RVSUM_1: 85;

      1 <= ( len f) by A17, A11, XXREAL_0: 2;

      then ( len f) in ( Seg ( len f)) by FINSEQ_1: 1;

      then

       A30: ( len f) in ( dom f) by FINSEQ_1:def 3;

      reconsider r = (f . ( len f)) as Real;

      

       A31: f = ((f | i) ^ (f /^ i)) by RFINSEQ: 8;

      for n,m be Element of NAT st n in ( dom (F | i)) & m in ( dom (F | i)) & ((F | i) /. n) = ((F | i) /. m) holds n = m

      proof

        

         A32: ( dom (F | i)) c= ( dom F) by FINSEQ_5: 18;

        let n,m be Element of NAT ;

        assume that

         A33: n in ( dom (F | i)) and

         A34: m in ( dom (F | i)) and

         A35: ((F | i) /. n) = ((F | i) /. m);

        (F /. n) = ((F | i) /. n) by A33, FINSEQ_4: 70

        .= (F /. m) by A34, A35, FINSEQ_4: 70;

        hence thesis by A1, A33, A34, A32, PARTFUN2: 10;

      end;

      then

       A36: (F | i) is one-to-one by PARTFUN2: 9;

      reconsider B = {v} as non empty Subset of V;

      consider L1 be Convex_Combination of V such that ( Sum L1) = v and

       A37: for A be non empty Subset of V st v in A holds L1 is Convex_Combination of A by Th1;

      

       A38: f = ((f | i) ^ (f /^ i)) by RFINSEQ: 8;

      set r9 = (1 / (1 - r));

      defpred P[ object, object] means ($1 in (( rng F) \ {v}) implies $2 = (r9 * (L . $1))) & ( not ($1 in (( rng F) \ {v})) implies $2 = 0 );

      

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

        x in (( rng F) \ {v}) or not x in (( rng F) \ {v});

        hence thesis;

      end;

      consider L2 be Function such that

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

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

      proof

        let y be object;

        assume y in ( rng L2);

        then

        consider x be object such that

         A41: x in ( dom L2) and

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

        per cases ;

          suppose

           A43: x in (( rng F) \ {v});

          then x in ( rng F);

          then

          reconsider x as VECTOR of V by A2;

          y = (r9 * (L . x)) by A40, A42, A43

          .= ((r9 * L) . x) by RLVECT_2:def 11;

          hence thesis;

        end;

          suppose not x in (( rng F) \ {v});

          then y = ( In ( 0 , REAL )) by A40, A41, A42;

          hence thesis;

        end;

      end;

      then ( rng L2) c= REAL ;

      then

       A44: L2 is Element of ( Funcs (the carrier of V, REAL )) by A40, FUNCT_2:def 2;

      ex T be finite Subset of V st for v be Element of V st not v in T holds (L2 . v) = 0

      proof

        reconsider T = (( Carrier L) \ {v}) as finite Subset of V;

        take T;

        thus thesis by A2, A40;

      end;

      then

      reconsider L2 as Linear_Combination of V by A44, RLVECT_2:def 3;

      for u be object st u in ( Carrier L2) holds u in (( Carrier L) \ {v})

      proof

        let u be object;

        assume

         A45: u in ( Carrier L2);

        then

        reconsider u as Element of V;

        (L2 . u) <> 0 by A45, RLVECT_2: 19;

        hence thesis by A2, A40;

      end;

      then

       A46: ( Carrier L2) c= (( Carrier L) \ {v});

      (f /^ i) = <*(f . ( len f))*> by A17, A12, FINSEQ_5: 30;

      then

       A47: ( Sum f) = (( Sum (f | i)) + r) by A31, RVSUM_1: 74;

      then ( Sum (f | i)) = (1 - r) by A18;

      then

       A48: 1 > (r + 0 ) by A29, XREAL_1: 20;

      

       A49: r9 > 0 by A18, A47, A29, XREAL_1: 139;

      for u be object st u in (( Carrier L) \ {v}) holds u in ( Carrier L2)

      proof

        let u be object;

        assume

         A50: u in (( Carrier L) \ {v});

        then

        reconsider u as Element of V;

        u in ( Carrier L) by A50, XBOOLE_0:def 5;

        then

         A51: (L . u) <> 0 by RLVECT_2: 19;

        (L2 . u) = (r9 * (L . u)) by A2, A40, A50;

        then (L2 . u) <> 0 by A49, A51, XCMPLX_1: 6;

        hence thesis by RLVECT_2: 19;

      end;

      then (( Carrier L) \ {v}) c= ( Carrier L2);

      then

       A52: ( Carrier L2) = (( Carrier L) \ {v}) by A46, XBOOLE_0:def 10;

      then ( Carrier L2) c= ( Carrier L) by XBOOLE_1: 36;

      then ( Carrier L2) c= M by A13;

      then

      reconsider L2 as Linear_Combination of M by RLVECT_2:def 6;

      deffunc F( set) = (L2 . ((F | i) . $1));

      consider f2 be FinSequence such that

       A53: ( len f2) = ( len (F | i)) & for k be Nat st k in ( dom f2) holds (f2 . k) = F(k) from FINSEQ_1:sch 2;

      F = ((F | i) ^ (F /^ i)) by RFINSEQ: 8;

      then ( Carrier L) = (( rng (F | i)) \/ ( rng (F /^ i))) by A2, FINSEQ_1: 31;

      then

       A54: (( Carrier L) \ ( rng (F /^ i))) = ( rng (F | i)) by A1, FINSEQ_5: 34, XBOOLE_1: 88;

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

      proof

        let y be object;

        

         A55: ex L29 be Function st L2 = L29 & ( dom L29) = the carrier of V & ( rng L29) c= REAL by FUNCT_2:def 2;

        assume y in ( rng f2);

        then

        consider x be object such that

         A56: x in ( dom f2) and

         A57: y = (f2 . x) by FUNCT_1:def 3;

        

         A58: x in ( Seg ( len f2)) by A56, FINSEQ_1:def 3;

        reconsider x as Element of NAT by A56;

        x in ( dom (F | i)) by A53, A58, FINSEQ_1:def 3;

        then ((F | i) . x) in ( rng (F | i)) by FUNCT_1: 3;

        then (L2 . ((F | i) . x)) in ( rng L2) by A54, A55, FUNCT_1: 3;

        then (L2 . ((F | i) . x)) in REAL ;

        hence thesis by A53, A56, A57;

      end;

      then ( rng f2) c= REAL ;

      then

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

      

       A59: ( dom f2) = ( Seg ( len (F | i))) by A53, FINSEQ_1:def 3;

      

      then

       A60: ( dom f2) = ( Seg i) by A12, FINSEQ_1: 59, NAT_1: 12

      .= ( Seg ( len (f | i))) by A17, A12, FINSEQ_1: 59, NAT_1: 12

      .= ( dom (f | i)) by FINSEQ_1:def 3;

      

       A61: (( len F) - 1) = i by A12;

      

       A62: for k be Element of NAT st k in ( dom f2) holds (f2 . k) = ((r9 * (f | i)) . k) & (f2 . k) >= 0

      proof

        let k be Element of NAT ;

        assume

         A63: k in ( dom f2);

        then

         A64: (f2 . k) = (L2 . ((F | i) . k)) by A53;

        k in ( dom (f | ( Seg i))) by A60, A63, FINSEQ_1:def 15;

        then k in (( dom f) /\ ( Seg i)) by RELAT_1: 61;

        then

         A65: k in ( dom f) by XBOOLE_0:def 4;

        

         A66: k in ( dom (F | i)) by A59, A63, FINSEQ_1:def 3;

        then ((F | i) . k) in ( rng (F | i)) by FUNCT_1: 3;

        then

        reconsider w = ((F | i) . k) as Element of V by A54;

        

         A67: (F | i) = (F | ( Seg i)) by FINSEQ_1:def 15;

        then

         A68: ((F | i) . k) = (F . k) by A66, FUNCT_1: 47;

        

         A69: not w in {v}

        proof

          k <= ( len (F | i)) & ( len (F | i)) <= i by A59, A63, FINSEQ_1: 1, FINSEQ_5: 17;

          then k <= i by XXREAL_0: 2;

          then

           A70: (k + 1) <= ( len F) by A61, XREAL_1: 19;

          assume w in {v};

          then

           A71: (F . k) = v by A68, TARSKI:def 1;

          ( dom (F | ( Seg i))) c= ( dom F) by RELAT_1: 60;

          then k = ( len F) by A1, A14, A66, A67, A71, FUNCT_1:def 4;

          hence contradiction by A70, NAT_1: 13;

        end;

        (f | i) = (f | ( Seg i)) by FINSEQ_1:def 15;

        then

         A72: ((f | i) . k) = (f . k) by A60, A63, FUNCT_1: 47;

        then

         A73: ((f | i) . k) = (L . (F . k)) by A19, A65;

        then

         A74: ((f | i) . k) = (L . ((F | i) . k)) by A66, A67, FUNCT_1: 47;

        per cases ;

          suppose

           A75: w in (( rng F) \ {v});

          (f . k) >= 0 by A19, A65;

          then

           A76: (r9 * ((f | i) . k)) >= 0 by A18, A47, A29, A72;

          (L2 . w) = (r9 * (L . w)) by A40, A75

          .= (r9 * ((f | i) . k)) by A73, A66, A67, FUNCT_1: 47

          .= ((r9 * (f | i)) . k) by RVSUM_1: 44;

          hence thesis by A64, A76, RVSUM_1: 44;

        end;

          suppose

           A77: not w in (( rng F) \ {v});

          then not w in ( rng F) by A69, XBOOLE_0:def 5;

          then (L . w) = 0 by A2, RLVECT_2: 19;

          then

           A78: (r9 * ((f | i) . k)) = 0 by A74;

          (f2 . k) = 0 by A40, A64, A77;

          hence thesis by A78, RVSUM_1: 44;

        end;

      end;

      then

       A79: for n be Nat st n in ( dom f2) holds (f2 . n) = (L2 . ((F | i) . n)) & (f2 . n) >= 0 by A53;

      (f /^ i) = <*(f . ( len f))*> by A17, A12, FINSEQ_5: 30;

      then

       A80: ( Sum f) = (( Sum (f | i)) + r) by A38, RVSUM_1: 74;

      (F /^ i) = <*(F . ( len F))*> by A12, FINSEQ_5: 30;

      then

       A81: ( rng (F | i)) = ( Carrier L2) by A52, A54, FINSEQ_1: 38;

      

       A82: for k be Nat st k in ( dom f2) holds (f2 . k) = ((r9 * (f | i)) . k) by A62;

      ( dom f2) = ( dom (r9 * (f | i))) by A60, VALUED_1:def 5;

      then f2 = (r9 * (f | i)) by A82, FINSEQ_1: 13;

      

      then ( Sum f2) = ((1 / (1 - r)) * (1 - r)) by A18, A80, RVSUM_1: 87

      .= (1 / ((1 - r) / (1 - r))) by XCMPLX_1: 81

      .= (1 / 1) by A18, A47, A29, XCMPLX_1: 60

      .= 1;

      then

      reconsider L2 as Convex_Combination of M by A36, A81, A53, A79, CONVEX1:def 3;

      

       A83: v in ( Carrier L) by A2, A14, FUNCT_1: 3;

      then {v} c= ( Carrier L) by ZFMISC_1: 31;

      then

       A84: ( card ( Carrier L2)) = (( card ( Carrier L)) - ( card {v})) by A52, CARD_2: 44;

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

      then

      reconsider L1 as Convex_Combination of M by A37, A83;

      v in {v} by TARSKI:def 1;

      then L1 is Convex_Combination of B by A37;

      then

       A85: ( Carrier L1) c= {v} by RLVECT_2:def 6;

      then

       A86: ( Carrier L1) = {} or ( Carrier L1) = {v} by ZFMISC_1: 33;

      

       A87: for u be Element of V holds (L . u) = (((r * L1) + ((1 - r) * L2)) . u)

      proof

        let u be Element of V;

        

         A88: (((r * L1) + ((1 - r) * L2)) . u) = (((r * L1) . u) + (((1 - r) * L2) . u)) by RLVECT_2:def 10;

        per cases ;

          suppose

           A89: u in ( Carrier L);

          per cases ;

            suppose

             A90: u = v;

            then u in {v} by TARSKI:def 1;

            then not u in ( Carrier L2) by A46, XBOOLE_0:def 5;

            then (L2 . u) = 0 by RLVECT_2: 19;

            then ((1 - r) * (L2 . u)) = 0 ;

            then

             A91: (((1 - r) * L2) . u) = 0 by RLVECT_2:def 11;

            (L1 . u) = 1 by A86, A90, CONVEX1: 21, CONVEX1: 27;

            then

             A92: (r * (L1 . u)) = r;

            (L . u) = (r + 0 ) by A17, A19, A30, A90;

            hence thesis by A88, A92, A91, RLVECT_2:def 11;

          end;

            suppose u <> v;

            then

             A93: not u in ( Carrier L1) by A85, TARSKI:def 1;

            then (L1 . u) = 0 by RLVECT_2: 19;

            then (r * (L1 . u)) = 0 ;

            then

             A94: ((r * L1) . u) = 0 by RLVECT_2:def 11;

            u in ( Carrier L2) by A52, A86, A89, A93, CONVEX1: 21, XBOOLE_0:def 5;

            then (L2 . u) = (r9 * (L . u)) by A2, A40, A46;

            

            then ((1 - r) * (L2 . u)) = (((1 - r) * r9) * (L . u))

            .= ((1 / ((1 - r) / (1 - r))) * (L . u)) by XCMPLX_1: 81

            .= (1 * (L . u)) by A18, A47, A29, XCMPLX_1: 51

            .= (L . u);

            hence thesis by A88, A94, RLVECT_2:def 11;

          end;

        end;

          suppose

           A95: not u in ( Carrier L);

          then not u in ( Carrier L1) by A2, A15, A85, TARSKI:def 1;

          then (L1 . u) = 0 by RLVECT_2: 19;

          then (r * (L1 . u)) = 0 ;

          then

           A96: ((r * L1) . u) = 0 by RLVECT_2:def 11;

           not u in ( Carrier L2) by A46, A95, XBOOLE_0:def 5;

          then (L2 . u) = 0 by RLVECT_2: 19;

          then

           A97: ((1 - r) * (L2 . u)) = 0 ;

          (L . u) = ( 0 + 0 ) by A95, RLVECT_2: 19;

          hence thesis by A88, A96, A97, RLVECT_2:def 11;

        end;

      end;

      take L1, L2, r;

      (f . ( len f)) = (L . (F . ( len f))) by A19, A30;

      then r <> 0 by A2, A17, A16, RLVECT_2: 19;

      hence thesis by A19, A30, A48, A86, A87, A84, CARD_1: 30, CONVEX1: 21, RLVECT_2:def 9;

    end;

    

     Lm3: for V be RealLinearSpace, M be non empty Subset of V st M is convex holds { ( Sum L) where L be Convex_Combination of M : L in ( ConvexComb V) } c= M

    proof

      let V be RealLinearSpace;

      let M be non empty Subset of V;

      set S = { ( Sum L) where L be Convex_Combination of M : L in ( ConvexComb V) };

      assume

       A1: M is convex;

      let v be object;

      assume v in S;

      then

      consider L be Convex_Combination of M such that

       A2: v = ( Sum L) and L in ( ConvexComb V);

      reconsider v as VECTOR of V by A2;

      per cases ;

        suppose

         A3: ( card ( Carrier L)) < 2;

        ( Carrier L) <> 0 by CONVEX1: 21;

        then

         A4: ( card ( Carrier L)) >= ( 0 + 1) by NAT_1: 13;

        ( card ( Carrier L)) < (1 + 1) by A3;

        then ( card ( Carrier L)) <= 1 by NAT_1: 13;

        then ( card ( Carrier L)) = 1 by A4, XXREAL_0: 1;

        then

        consider x be object such that

         A5: ( Carrier L) = {x} by CARD_2: 42;

        x in ( Carrier L) by A5, TARSKI:def 1;

        then

        reconsider x as VECTOR of V;

        

         A6: {x} c= M by A5, RLVECT_2:def 6;

        v = ((L . x) * x) by A2, A5, RLVECT_2: 35

        .= (1 * x) by A5, CONVEX1: 27

        .= x by RLVECT_1:def 8;

        hence thesis by A6, ZFMISC_1: 31;

      end;

        suppose

         A7: ( card ( Carrier L)) >= 2;

        defpred P[ Nat] means for LL be Convex_Combination of M st ( card ( Carrier LL)) = (1 + $1) & (ex L1,L2 be Convex_Combination of M, r be Real st 0 < r & r < 1 & LL = ((r * L1) + ((1 - r) * L2)) & ( card ( Carrier L1)) = 1 & ( card ( Carrier L2)) = (( card ( Carrier LL)) - 1)) holds ( Sum LL) in M;

        

         A8: P[1]

        proof

          let LL be Convex_Combination of M;

          assume that

           A9: ( card ( Carrier LL)) = (1 + 1) and

           A10: ex L1,L2 be Convex_Combination of M, r be Real st 0 < r & r < 1 & LL = ((r * L1) + ((1 - r) * L2)) & ( card ( Carrier L1)) = 1 & ( card ( Carrier L2)) = (( card ( Carrier LL)) - 1);

          consider L1,L2 be Convex_Combination of M, r be Real such that

           A11: 0 < r & r < 1 and

           A12: LL = ((r * L1) + ((1 - r) * L2)) and

           A13: ( card ( Carrier L1)) = 1 and

           A14: ( card ( Carrier L2)) = (( card ( Carrier LL)) - 1) by A10;

          consider x2 be object such that

           A15: ( Carrier L2) = {x2} by A9, A14, CARD_2: 42;

          x2 in ( Carrier L2) by A15, TARSKI:def 1;

          then

          reconsider x2 as VECTOR of V;

          ( Sum L2) = ((L2 . x2) * x2) & (L2 . x2) = 1 by A15, CONVEX1: 27, RLVECT_2: 35;

          then

           A16: ( Sum L2) = x2 by RLVECT_1:def 8;

           {x2} c= M by A15, RLVECT_2:def 6;

          then

           A17: ( Sum L2) in M by A16, ZFMISC_1: 31;

          consider x1 be object such that

           A18: ( Carrier L1) = {x1} by A13, CARD_2: 42;

          x1 in ( Carrier L1) by A18, TARSKI:def 1;

          then

          reconsider x1 as VECTOR of V;

          ( Sum L1) = ((L1 . x1) * x1) & (L1 . x1) = 1 by A18, CONVEX1: 27, RLVECT_2: 35;

          then

           A19: ( Sum L1) = x1 by RLVECT_1:def 8;

           {x1} c= M by A18, RLVECT_2:def 6;

          then

           A20: ( Sum L1) in M by A19, ZFMISC_1: 31;

          ( Sum LL) = (( Sum (r * L1)) + ( Sum ((1 - r) * L2))) by A12, RLVECT_3: 1

          .= ((r * ( Sum L1)) + ( Sum ((1 - r) * L2))) by RLVECT_3: 2

          .= ((r * ( Sum L1)) + ((1 - r) * ( Sum L2))) by RLVECT_3: 2;

          hence thesis by A1, A11, A20, A17, CONVEX1:def 2;

        end;

        consider k be Nat such that

         A21: ( card ( Carrier L)) = (k + 1) by A7, NAT_1: 6;

        reconsider k as non zero Element of NAT by A7, A21, ORDINAL1:def 12;

        

         A22: ( card ( Carrier L)) = (1 + k) by A21;

        

         A23: ex L1,L2 be Convex_Combination of M, r be Real st 0 < r & r < 1 & L = ((r * L1) + ((1 - r) * L2)) & ( card ( Carrier L1)) = 1 & ( card ( Carrier L2)) = (( card ( Carrier L)) - 1) by A7, Lm2;

        

         A24: for k be non zero Nat st P[k] holds P[(k + 1)]

        proof

          let k be non zero Nat;

          assume

           A25: P[k];

          let LL be Convex_Combination of M;

          assume that

           A26: ( card ( Carrier LL)) = (1 + (k + 1)) and

           A27: ex L1,L2 be Convex_Combination of M, r be Real st 0 < r & r < 1 & LL = ((r * L1) + ((1 - r) * L2)) & ( card ( Carrier L1)) = 1 & ( card ( Carrier L2)) = (( card ( Carrier LL)) - 1);

          consider L1,L2 be Convex_Combination of M, r be Real such that

           A28: 0 < r & r < 1 and

           A29: LL = ((r * L1) + ((1 - r) * L2)) and

           A30: ( card ( Carrier L1)) = 1 and

           A31: ( card ( Carrier L2)) = (( card ( Carrier LL)) - 1) by A27;

          k >= ( 0 + 1) by NAT_1: 13;

          then (k + 1) >= (1 + 1) by XREAL_1: 6;

          then ex LL1,LL2 be Convex_Combination of M, rr be Real st 0 < rr & rr < 1 & L2 = ((rr * LL1) + ((1 - rr) * LL2)) & ( card ( Carrier LL1)) = 1 & ( card ( Carrier LL2)) = (( card ( Carrier L2)) - 1) by A26, A31, Lm2;

          then

           A32: ( Sum L2) in M by A25, A26, A31;

          consider x1 be object such that

           A33: ( Carrier L1) = {x1} by A30, CARD_2: 42;

          x1 in ( Carrier L1) by A33, TARSKI:def 1;

          then

          reconsider x1 as VECTOR of V;

          ( Sum L1) = ((L1 . x1) * x1) & (L1 . x1) = 1 by A33, CONVEX1: 27, RLVECT_2: 35;

          then

           A34: ( Sum L1) = x1 by RLVECT_1:def 8;

           {x1} c= M by A33, RLVECT_2:def 6;

          then

           A35: ( Sum L1) in M by A34, ZFMISC_1: 31;

          ( Sum LL) = (( Sum (r * L1)) + ( Sum ((1 - r) * L2))) by A29, RLVECT_3: 1

          .= ((r * ( Sum L1)) + ( Sum ((1 - r) * L2))) by RLVECT_3: 2

          .= ((r * ( Sum L1)) + ((1 - r) * ( Sum L2))) by RLVECT_3: 2;

          hence thesis by A1, A28, A35, A32, CONVEX1:def 2;

        end;

        for k be non zero Nat holds P[k] from NAT_1:sch 10( A8, A24);

        hence thesis by A2, A22, A23;

      end;

    end;

    theorem :: CONVEX3:4

    for V be RealLinearSpace, M be non empty Subset of V holds M is convex iff { ( Sum L) where L be Convex_Combination of M : L in ( ConvexComb V) } c= M by Lm1, Lm3;

    theorem :: CONVEX3:5

    for V be RealLinearSpace, M be non empty Subset of V holds ( conv M) = { ( Sum L) where L be Convex_Combination of M : L in ( ConvexComb V) }

    proof

      let V be RealLinearSpace;

      let M be non empty Subset of V;

      consider m be object such that

       A1: m in M by XBOOLE_0:def 1;

      reconsider m as VECTOR of V by A1;

      consider LL be Convex_Combination of V such that

       A2: ( Sum LL) = m and

       A3: for A be non empty Subset of V st m in A holds LL is Convex_Combination of A by Th1;

      reconsider LL as Convex_Combination of M by A1, A3;

      LL in ( ConvexComb V) by Def1;

      then m in { ( Sum L) where L be Convex_Combination of M : L in ( ConvexComb V) } by A2;

      then

      reconsider N = { ( Sum L) where L be Convex_Combination of M : L in ( ConvexComb V) } as non empty set;

      for x be object st x in N holds x in the carrier of V

      proof

        let x be object;

        assume x in N;

        then ex L be Convex_Combination of M st x = ( Sum L) & L in ( ConvexComb V);

        hence thesis;

      end;

      then

      reconsider N as Subset of V by TARSKI:def 3;

      for x be object st x in { ( Sum L) where L be Convex_Combination of M : L in ( ConvexComb V) } holds x in ( conv M)

      proof

        let x be object;

        assume x in { ( Sum L) where L be Convex_Combination of M : L in ( ConvexComb V) };

        then

         A4: ex L be Convex_Combination of M st x = ( Sum L) & L in ( ConvexComb V);

        M c= ( conv M) by CONVEX1: 41;

        hence thesis by A4, CONVEX2: 6;

      end;

      then

       A5: { ( Sum L) where L be Convex_Combination of M : L in ( ConvexComb V) } c= ( conv M);

      for u,v be VECTOR of V, r be Real st 0 < r & r < 1 & u in N & v in N holds ((r * u) + ((1 - r) * v)) in N

      proof

        let u,v be VECTOR of V;

        let r be Real;

        assume that

         A6: 0 < r & r < 1 and

         A7: u in N and

         A8: v in N;

        consider Lv be Convex_Combination of M such that

         A9: v = ( Sum Lv) and Lv in ( ConvexComb V) by A8;

        consider Lu be Convex_Combination of M such that

         A10: u = ( Sum Lu) and Lu in ( ConvexComb V) by A7;

        reconsider r as Real;

        reconsider LL = ((r * Lu) + ((1 - r) * Lv)) as Convex_Combination of M by A6, CONVEX2: 9;

        ((r * Lu) + ((1 - r) * Lv)) is Convex_Combination of V by A6, CONVEX2: 8;

        then

         A11: ((r * Lu) + ((1 - r) * Lv)) in ( ConvexComb V) by Def1;

        ( Sum LL) = (( Sum (r * Lu)) + ( Sum ((1 - r) * Lv))) by RLVECT_3: 1

        .= ((r * ( Sum Lu)) + ( Sum ((1 - r) * Lv))) by RLVECT_3: 2

        .= ((r * ( Sum Lu)) + ((1 - r) * ( Sum Lv))) by RLVECT_3: 2;

        hence thesis by A10, A9, A11;

      end;

      then

       A12: N is convex by CONVEX1:def 2;

      for v be object st v in M holds v in N

      proof

        let v be object;

        assume

         A13: v in M;

        then

        reconsider v as VECTOR of V;

        consider LL be Convex_Combination of V such that

         A14: ( Sum LL) = v and

         A15: for A be non empty Subset of V st v in A holds LL is Convex_Combination of A by Th1;

        reconsider LL as Convex_Combination of M by A13, A15;

        LL in ( ConvexComb V) by Def1;

        hence thesis by A14;

      end;

      then M c= N;

      then ( conv M) c= N by A12, CONVEX1: 30;

      hence thesis by A5, XBOOLE_0:def 10;

    end;

    begin

    definition

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

      :: CONVEX3:def3

      attr M is cone means

      : Def3: for r be Real, v be VECTOR of V st r > 0 & v in M holds (r * v) in M;

    end

    theorem :: CONVEX3:6

    

     Th6: for V be non empty RLSStruct, M be Subset of V st M = {} holds M is cone;

    registration

      let V be non empty RLSStruct;

      cluster cone for Subset of V;

      existence

      proof

        ( {} V) is cone;

        hence thesis;

      end;

    end

    registration

      let V be non empty RLSStruct;

      cluster empty cone for Subset of V;

      existence

      proof

        set M = {} ;

        reconsider M as Subset of V by XBOOLE_1: 2;

        reconsider M as cone Subset of V by Th6;

        take M;

        thus thesis;

      end;

    end

    registration

      let V be RealLinearSpace;

      cluster non empty cone for Subset of V;

      existence

      proof

        set M = {( 0. V)};

        reconsider M as Subset of V;

        for r be Real, v be VECTOR of V st r > 0 & v in M holds (r * v) in M

        proof

          let r be Real;

          let v be VECTOR of V;

          assume that r > 0 and

           A1: v in M;

          v = ( 0. V) by A1, TARSKI:def 1;

          then (r * v) = ( 0. V);

          hence thesis by TARSKI:def 1;

        end;

        then

        reconsider M as cone Subset of V by Def3;

        take M;

        thus thesis;

      end;

    end

    theorem :: CONVEX3:7

    

     Th7: for V be non empty RLSStruct, M be cone Subset of V st V is vector-distributive scalar-distributive scalar-associative scalar-unital holds M is convex iff for u,v be VECTOR of V st u in M & v in M holds (u + v) in M

    proof

      let V be non empty RLSStruct;

      let M be cone Subset of V;

      

       A1: (for u,v be VECTOR of V st u in M & v in M holds (u + v) in M) implies M is convex

      proof

        assume

         A2: for u,v be VECTOR of V st u in M & v in M holds (u + v) in M;

        for u,v be VECTOR of V, r be Real st 0 < r & r < 1 & u in M & v in M holds ((r * u) + ((1 - r) * v)) in M

        proof

          let u,v be VECTOR of V;

          let r be Real;

          assume that

           A3: 0 < r and

           A4: r < 1 and

           A5: u in M and

           A6: v in M;

          reconsider r as Real;

          (r + 0 ) < 1 by A4;

          then (1 - r) > 0 by XREAL_1: 20;

          then

           A7: ((1 - r) * v) in M by A6, Def3;

          (r * u) in M by A3, A5, Def3;

          hence thesis by A2, A7;

        end;

        hence thesis by CONVEX1:def 2;

      end;

      assume

       A8: V is vector-distributive scalar-distributive scalar-associative scalar-unital;

      M is convex implies for u,v be VECTOR of V st u in M & v in M holds (u + v) in M

      proof

        assume

         A9: M is convex;

        for u,v be VECTOR of V st u in M & v in M holds (u + v) in M

        proof

          let u,v be VECTOR of V;

          assume u in M & v in M;

          then (((1 / 2) * u) + ((1 - (1 / 2)) * v)) in M by A9, CONVEX1:def 2;

          then

           A10: (2 * ((jd * u) + (jd * v))) in M by Def3;

          (2 * (((1 / 2) * u) + ((1 / 2) * v))) = ((2 * ((1 / 2) * u)) + (2 * ((1 / 2) * v))) by A8, RLVECT_1:def 5

          .= (((2 * (1 / 2)) * u) + (2 * ((1 / 2) * v))) by A8, RLVECT_1:def 7

          .= ((1 * u) + ((2 * (1 / 2)) * v)) by A8, RLVECT_1:def 7

          .= (u + (1 * v)) by A8, RLVECT_1:def 8;

          hence thesis by A8, A10, RLVECT_1:def 8;

        end;

        hence thesis;

      end;

      hence thesis by A1;

    end;

    

     Lm4: for V be RealLinearSpace, M be Subset of V, L be Linear_Combination of M st ( card ( Carrier L)) >= 1 holds ex L1,L2 be Linear_Combination of M st ( Sum L) = (( Sum L1) + ( Sum L2)) & ( card ( Carrier L1)) = 1 & ( card ( Carrier L2)) = (( card ( Carrier L)) - 1) & ( Carrier L1) c= ( Carrier L) & ( Carrier L2) c= ( Carrier L) & (for v be VECTOR of V st v in ( Carrier L1) holds (L1 . v) = (L . v)) & for v be VECTOR of V st v in ( Carrier L2) holds (L2 . v) = (L . v)

    proof

      let V be RealLinearSpace;

      let M be Subset of V;

      let L be Linear_Combination of M;

      assume ( card ( Carrier L)) >= 1;

      then ( Carrier L) <> {} ;

      then

      consider u be object such that

       A1: u in ( Carrier L) by XBOOLE_0:def 1;

      reconsider u as VECTOR of V by A1;

      consider L1 be Linear_Combination of {u} such that

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

      

       A3: ( Carrier L1) c= {u} by RLVECT_2:def 6;

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

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

      then ( Carrier L1) c= M by A3;

      then

      reconsider L1 as Linear_Combination of M by RLVECT_2:def 6;

      

       A4: for v be VECTOR of V st v in ( Carrier L1) holds (L1 . v) = (L . v)

      proof

        let v be VECTOR of V;

        assume v in ( Carrier L1);

        then v = u by A3, TARSKI:def 1;

        hence thesis by A2;

      end;

      defpred P[ object, object] means ($1 in (( Carrier L) \ {u}) implies $2 = (L . $1)) & ( not ($1 in (( Carrier L) \ {u})) implies $2 = 0 );

      

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

        x in (( Carrier L) \ {u}) or not x in (( Carrier L) \ {u});

        hence thesis;

      end;

      consider L2 be Function such that

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

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

      proof

        let y be object;

        assume y in ( rng L2);

        then

        consider x be object such that

         A7: x in ( dom L2) and

         A8: y = (L2 . x) by FUNCT_1:def 3;

        per cases ;

          suppose

           A9: x in (( Carrier L) \ {u});

          then

          reconsider x as VECTOR of V;

          y = (L . x) by A6, A8, A9;

          hence thesis;

        end;

          suppose not x in (( Carrier L) \ {u});

          then y = ( In ( 0 , REAL )) by A6, A7, A8;

          hence thesis;

        end;

      end;

      then ( rng L2) c= REAL ;

      then

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

      ex T be finite Subset of V st for v be Element of V st not v in T holds (L2 . v) = 0

      proof

        set T = (( Carrier L) \ {u});

        reconsider T as finite Subset of V;

        take T;

        thus thesis by A6;

      end;

      then

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

      for x be object st x in ( Carrier L2) holds x in M

      proof

        let x be object;

        assume

         A11: x in ( Carrier L2);

        then

        reconsider x as VECTOR of V;

        (L2 . x) <> 0 by A11, RLVECT_2: 19;

        then x in (( Carrier L) \ {u}) by A6;

        then

         A12: x in ( Carrier L) by XBOOLE_0:def 5;

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

        hence thesis by A12;

      end;

      then ( Carrier L2) c= M;

      then

      reconsider L2 as Linear_Combination of M by RLVECT_2:def 6;

      for x be object st x in ( Carrier L2) holds x in (( Carrier L) \ {u})

      proof

        let x be object;

        assume

         A13: x in ( Carrier L2);

        then

        reconsider x as VECTOR of V;

        (L2 . x) <> 0 by A13, RLVECT_2: 19;

        hence thesis by A6;

      end;

      then

       A14: ( Carrier L2) c= (( Carrier L) \ {u});

      for v be VECTOR of V holds (L . v) = ((L1 + L2) . v)

      proof

        let v be VECTOR of V;

        per cases ;

          suppose

           A15: v in ( Carrier L);

          per cases ;

            suppose

             A16: v = u;

            then

             A17: not v in ( Carrier L2) by A14, ZFMISC_1: 56;

            ((L1 + L2) . v) = ((L1 . v) + (L2 . v)) by RLVECT_2:def 10

            .= ((L . v) + 0 ) by A2, A16, A17, RLVECT_2: 19;

            hence thesis;

          end;

            suppose

             A18: v <> u;

            then not v in ( Carrier L1) by A3, TARSKI:def 1;

            then

             A19: (L1 . v) = 0 by RLVECT_2: 19;

            

             A20: v in (( Carrier L) \ {u}) by A15, A18, ZFMISC_1: 56;

            ((L1 + L2) . v) = ((L1 . v) + (L2 . v)) by RLVECT_2:def 10

            .= ( 0 + (L . v)) by A6, A19, A20;

            hence thesis;

          end;

        end;

          suppose

           A21: not v in ( Carrier L);

          then not v in ( Carrier L2) by A14, ZFMISC_1: 56;

          then

           A22: (L2 . v) = 0 by RLVECT_2: 19;

          

           A23: not v in ( Carrier L1) by A1, A3, A21, TARSKI:def 1;

          ((L1 + L2) . v) = ((L1 . v) + (L2 . v)) by RLVECT_2:def 10

          .= 0 by A23, A22, RLVECT_2: 19;

          hence thesis by A21, RLVECT_2: 19;

        end;

      end;

      then

       A24: L = (L1 + L2) by RLVECT_2:def 9;

      for x be object st x in (( Carrier L) \ {u}) holds x in ( Carrier L2)

      proof

        let x be object;

        assume

         A25: x in (( Carrier L) \ {u});

        then

        reconsider x as VECTOR of V;

        x in ( Carrier L) by A25, XBOOLE_0:def 5;

        then

         A26: (L . x) <> 0 by RLVECT_2: 19;

        (L2 . x) = (L . x) by A6, A25;

        hence thesis by A26, RLVECT_2: 19;

      end;

      then (( Carrier L) \ {u}) c= ( Carrier L2);

      then

       A27: ( Carrier L2) = (( Carrier L) \ {u}) by A14, XBOOLE_0:def 10;

      take L1, L2;

      

       A28: (( Carrier L) \ {u}) c= ( Carrier L) by XBOOLE_1: 36;

      ( Carrier L1) <> {}

      proof

        assume ( Carrier L1) = {} ;

        then (L . u) = 0 by A2, RLVECT_2: 19;

        hence contradiction by A1, RLVECT_2: 19;

      end;

      then

       A29: ( Carrier L1) = {u} by A3, ZFMISC_1: 33;

      then ( Carrier L1) c= ( Carrier L) by A1, ZFMISC_1: 31;

      

      then ( card ( Carrier L2)) = (( card ( Carrier L)) - ( card ( Carrier L1))) by A29, A27, CARD_2: 44

      .= (( card ( Carrier L)) - 1) by A29, CARD_1: 30;

      hence thesis by A1, A4, A6, A29, A14, A24, A28, CARD_1: 30, RLVECT_3: 1, ZFMISC_1: 31;

    end;

    theorem :: CONVEX3:8

    for V be RealLinearSpace, M be Subset of V holds M is convex & M is cone iff for L be Linear_Combination of M st ( Carrier L) <> {} & for v be VECTOR of V st v in ( Carrier L) holds (L . v) > 0 holds ( Sum L) in M

    proof

      let V be RealLinearSpace;

      let M be Subset of V;

      

       A1: (for L be Linear_Combination of M st ( Carrier L) <> {} & for v be VECTOR of V st v in ( Carrier L) holds (L . v) > 0 holds ( Sum L) in M) implies M is convex & M is cone

      proof

        assume

         A2: for L be Linear_Combination of M st ( Carrier L) <> {} & for v be VECTOR of V st v in ( Carrier L) holds (L . v) > 0 holds ( Sum L) in M;

        

         A3: for r be Real, v be VECTOR of V st r > 0 & v in M holds (r * v) in M

        proof

          let r be Real;

          let v be VECTOR of V;

          assume that

           A4: r > 0 and

           A5: v in M;

          reconsider r as Real;

          consider L be Linear_Combination of {v} such that

           A6: (L . v) = r by RLVECT_4: 37;

          

           A7: for u be VECTOR of V st u in ( Carrier L) holds (L . u) > 0

          proof

            let u be VECTOR of V;

            

             A8: ( Carrier L) c= {v} by RLVECT_2:def 6;

            assume u in ( Carrier L);

            hence thesis by A4, A6, A8, TARSKI:def 1;

          end;

          

           A9: v in ( Carrier L) by A4, A6, RLVECT_2: 19;

           {v} c= M by A5, ZFMISC_1: 31;

          then

          reconsider L as Linear_Combination of M by RLVECT_2: 21;

          ( Sum L) in M by A2, A9, A7;

          hence thesis by A6, RLVECT_2: 32;

        end;

        

         A10: for u,v be VECTOR of V st u in M & v in M holds (u + v) in M

        proof

          let u,v be VECTOR of V;

          assume that

           A11: u in M and

           A12: v in M;

          per cases ;

            suppose

             A13: u <> v;

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

             A14: (L . u) = jj & (L . v) = jj by A13, RLVECT_4: 38;

            

             A15: ( Sum L) = ((1 * u) + (1 * v)) by A13, A14, RLVECT_2: 33

            .= (u + (1 * v)) by RLVECT_1:def 8

            .= (u + v) by RLVECT_1:def 8;

            

             A16: ( Carrier L) <> {} by A14, RLVECT_2: 19;

            

             A17: for v1 be VECTOR of V st v1 in ( Carrier L) holds (L . v1) > 0

            proof

              let v1 be VECTOR of V;

              

               A18: ( Carrier L) c= {u, v} by RLVECT_2:def 6;

              assume

               A19: v1 in ( Carrier L);

              per cases by A19, A18, TARSKI:def 2;

                suppose v1 = u;

                hence thesis by A14;

              end;

                suppose v1 = v;

                hence thesis by A14;

              end;

            end;

             {u, v} c= M by A11, A12, ZFMISC_1: 32;

            then

            reconsider L as Linear_Combination of M by RLVECT_2: 21;

            ( Sum L) in M by A2, A16, A17;

            hence thesis by A15;

          end;

            suppose

             A20: u = v;

            ((jj + jj) * u) in M by A3, A11;

            then ((1 * u) + (1 * u)) in M by RLVECT_1:def 6;

            then (u + (1 * u)) in M by RLVECT_1:def 8;

            hence thesis by A20, RLVECT_1:def 8;

          end;

        end;

        M is cone by A3;

        hence thesis by A10, Th7;

      end;

      M is convex & M is cone implies for L be Linear_Combination of M st ( Carrier L) <> {} & (for v be VECTOR of V st v in ( Carrier L) holds (L . v) > 0 ) holds ( Sum L) in M

      proof

        defpred P[ Nat] means for LL be Linear_Combination of M st ( card ( Carrier LL)) = $1 & (for u be VECTOR of V st u in ( Carrier LL) holds (LL . u) > 0 ) & (ex L1,L2 be Linear_Combination of M st ( Sum LL) = (( Sum L1) + ( Sum L2)) & ( card ( Carrier L1)) = 1 & ( card ( Carrier L2)) = (( card ( Carrier LL)) - 1) & ( Carrier L1) c= ( Carrier LL) & ( Carrier L2) c= ( Carrier LL) & (for v be VECTOR of V st v in ( Carrier L1) holds (L1 . v) = (LL . v)) & (for v be VECTOR of V st v in ( Carrier L2) holds (L2 . v) = (LL . v))) holds ( Sum LL) in M;

        assume that

         A21: M is convex and

         A22: M is cone;

        

         A23: P[1]

        proof

          let LL be Linear_Combination of M;

          assume that

           A24: ( card ( Carrier LL)) = 1 and

           A25: for u be VECTOR of V st u in ( Carrier LL) holds (LL . u) > 0 and ex L1,L2 be Linear_Combination of M st ( Sum LL) = (( Sum L1) + ( Sum L2)) & ( card ( Carrier L1)) = 1 & ( card ( Carrier L2)) = (( card ( Carrier LL)) - 1) & ( Carrier L1) c= ( Carrier LL) & ( Carrier L2) c= ( Carrier LL) & (for v be VECTOR of V st v in ( Carrier L1) holds (L1 . v) = (LL . v)) & for v be VECTOR of V st v in ( Carrier L2) holds (L2 . v) = (LL . v);

          consider x be object such that

           A26: ( Carrier LL) = {x} by A24, CARD_2: 42;

           {x} c= M by A26, RLVECT_2:def 6;

          then

           A27: x in M by ZFMISC_1: 31;

          then

          reconsider x as VECTOR of V;

          x in ( Carrier LL) by A26, TARSKI:def 1;

          then

           A28: (LL . x) > 0 by A25;

          ( Sum LL) = ((LL . x) * x) by A26, RLVECT_2: 35;

          hence thesis by A22, A27, A28;

        end;

        

         A29: for k be non zero Nat st P[k] holds P[(k + 1)]

        proof

          let k be non zero Nat;

          assume

           A30: P[k];

          let LL be Linear_Combination of M;

          assume that

           A31: ( card ( Carrier LL)) = (k + 1) and

           A32: for u be VECTOR of V st u in ( Carrier LL) holds (LL . u) > 0 and

           A33: ex L1,L2 be Linear_Combination of M st ( Sum LL) = (( Sum L1) + ( Sum L2)) & ( card ( Carrier L1)) = 1 & ( card ( Carrier L2)) = (( card ( Carrier LL)) - 1) & ( Carrier L1) c= ( Carrier LL) & ( Carrier L2) c= ( Carrier LL) & (for v be VECTOR of V st v in ( Carrier L1) holds (L1 . v) = (LL . v)) & for v be VECTOR of V st v in ( Carrier L2) holds (L2 . v) = (LL . v);

          consider L1,L2 be Linear_Combination of M such that

           A34: ( Sum LL) = (( Sum L1) + ( Sum L2)) and

           A35: ( card ( Carrier L1)) = 1 and

           A36: ( card ( Carrier L2)) = (( card ( Carrier LL)) - 1) and

           A37: ( Carrier L1) c= ( Carrier LL) and

           A38: ( Carrier L2) c= ( Carrier LL) and

           A39: for v be VECTOR of V st v in ( Carrier L1) holds (L1 . v) = (LL . v) and

           A40: for v be VECTOR of V st v in ( Carrier L2) holds (L2 . v) = (LL . v) by A33;

          

           A41: for u be VECTOR of V st u in ( Carrier L1) holds (L1 . u) > 0

          proof

            let u be VECTOR of V;

            assume

             A42: u in ( Carrier L1);

            then (L1 . u) = (LL . u) by A39;

            hence thesis by A32, A37, A42;

          end;

          

           A43: for u be VECTOR of V st u in ( Carrier L2) holds (L2 . u) > 0

          proof

            let u be VECTOR of V;

            assume

             A44: u in ( Carrier L2);

            then (L2 . u) = (LL . u) by A40;

            hence thesis by A32, A38, A44;

          end;

          ex LL1,LL2 be Linear_Combination of M st ( Sum L1) = (( Sum LL1) + ( Sum LL2)) & ( card ( Carrier LL1)) = 1 & ( card ( Carrier LL2)) = (( card ( Carrier L1)) - 1) & ( Carrier LL1) c= ( Carrier L1) & ( Carrier LL2) c= ( Carrier L1) & (for v be VECTOR of V st v in ( Carrier LL1) holds (LL1 . v) = (L1 . v)) & for v be VECTOR of V st v in ( Carrier LL2) holds (LL2 . v) = (L1 . v) by A35, Lm4;

          then

           A45: ( Sum L1) in M by A23, A35, A41;

          ( card ( Carrier L2)) >= ( 0 + 1) by A31, A36, NAT_1: 13;

          then ex LL1,LL2 be Linear_Combination of M st ( Sum L2) = (( Sum LL1) + ( Sum LL2)) & ( card ( Carrier LL1)) = 1 & ( card ( Carrier LL2)) = (( card ( Carrier L2)) - 1) & ( Carrier LL1) c= ( Carrier L2) & ( Carrier LL2) c= ( Carrier L2) & (for v be VECTOR of V st v in ( Carrier LL1) holds (LL1 . v) = (L2 . v)) & for v be VECTOR of V st v in ( Carrier LL2) holds (LL2 . v) = (L2 . v) by Lm4;

          then ( Sum L2) in M by A30, A31, A36, A43;

          hence thesis by A21, A22, A34, A45, Th7;

        end;

        

         A46: for k be non zero Nat holds P[k] from NAT_1:sch 10( A23, A29);

        let L be Linear_Combination of M;

        assume that

         A47: ( Carrier L) <> {} and

         A48: for v be VECTOR of V st v in ( Carrier L) holds (L . v) > 0 ;

        ( card ( Carrier L)) >= ( 0 + 1) by A47, NAT_1: 13;

        then ex L1,L2 be Linear_Combination of M st ( Sum L) = (( Sum L1) + ( Sum L2)) & ( card ( Carrier L1)) = 1 & ( card ( Carrier L2)) = (( card ( Carrier L)) - 1) & ( Carrier L1) c= ( Carrier L) & ( Carrier L2) c= ( Carrier L) & (for v be VECTOR of V st v in ( Carrier L1) holds (L1 . v) = (L . v)) & for v be VECTOR of V st v in ( Carrier L2) holds (L2 . v) = (L . v) by Lm4;

        hence thesis by A47, A48, A46;

      end;

      hence thesis by A1;

    end;

    theorem :: CONVEX3:9

    for V be non empty RLSStruct, M,N be Subset of V st M is cone & N is cone holds (M /\ N) is cone

    proof

      let V be non empty RLSStruct;

      let M,N be Subset of V;

      assume that

       A1: M is cone and

       A2: N is cone;

      let r be Real;

      let v be VECTOR of V;

      assume that

       A3: r > 0 and

       A4: v in (M /\ N);

      v in N by A4, XBOOLE_0:def 4;

      then

       A5: (r * v) in N by A2, A3;

      v in M by A4, XBOOLE_0:def 4;

      then (r * v) in M by A1, A3;

      hence thesis by A5, XBOOLE_0:def 4;

    end;