convex4.miz



    begin

    definition

      let V be non empty 1-sorted;

      :: CONVEX4:def1

      mode C_Linear_Combination of V -> Element of ( Funcs (the carrier of V, COMPLEX )) means

      : Def1: ex T be finite Subset of V st for v be Element of V st not v in T holds (it . v) = 0 ;

      existence

      proof

        reconsider f = (the carrier of V --> 0c ) as Element of ( Funcs (the carrier of V, COMPLEX )) by FUNCT_2: 8;

        take f, ( {} V);

        thus thesis by FUNCOP_1: 7;

      end;

    end

    notation

      let V be non empty addLoopStr, L be Element of ( Funcs (the carrier of V, COMPLEX ));

      synonym Carrier L for support L;

    end

     Lm1:

    now

      let V be non empty addLoopStr, L be Element of ( Funcs (the carrier of V, COMPLEX ));

      

       A1: ( support L) c= ( dom L) by PRE_POLY: 37;

      thus ( Carrier L) c= the carrier of V

      proof

        let x be object;

        assume x in ( support L);

        then x in ( dom L) by A1;

        hence thesis;

      end;

    end;

    definition

      let V be non empty addLoopStr, L be Element of ( Funcs (the carrier of V, COMPLEX ));

      :: original: Carrier

      redefine

      :: CONVEX4:def2

      func Carrier L -> Subset of V equals { v where v be Element of V : (L . v) <> 0c };

      coherence by Lm1;

      compatibility

      proof

        let X be Subset of V;

        set A = ( Carrier L);

        set B = { v where v be Element of V : (L . v) <> 0 };

        thus X = A implies X = B

        proof

          assume

           A1: X = A;

          thus X c= B

          proof

            let x be object;

            assume

             A2: x in X;

            then (L . x) <> 0 by A1, PRE_POLY:def 7;

            hence thesis by A2;

          end;

          let x be object;

          assume x in B;

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

          hence thesis by A1, PRE_POLY:def 7;

        end;

        assume

         A3: X = B;

        thus X c= A

        proof

          let x be object;

          assume x in X;

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

          hence thesis by PRE_POLY:def 7;

        end;

        let x be object;

        assume

         A4: x in A;

        then

         A5: (L . x) <> 0 by PRE_POLY:def 7;

        ( Carrier L) c= the carrier of V by Lm1;

        hence thesis by A3, A4, A5;

      end;

    end

    registration

      let V be non empty addLoopStr, L be C_Linear_Combination of V;

      cluster ( Carrier L) -> finite;

      coherence

      proof

        set A = ( Carrier L);

        consider T be finite Subset of V such that

         A1: for v be Element of V st not v in T holds (L . v) = 0c by Def1;

        now

          let x be object;

          assume x in A;

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

          hence x in T by A1;

        end;

        then A c= T;

        hence thesis;

      end;

    end

    theorem :: CONVEX4:1

    

     Th1: for V be non empty addLoopStr, L be C_Linear_Combination of V, v be Element of V holds (L . v) = 0c iff not v in ( Carrier L)

    proof

      let V be non empty addLoopStr, L be C_Linear_Combination of V, v be Element of V;

      thus (L . v) = 0c implies not v in ( Carrier L)

      proof

        assume

         A1: (L . v) = 0c ;

        assume not thesis;

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

        hence thesis by A1;

      end;

      thus thesis;

    end;

    definition

      let V be non empty addLoopStr;

      :: CONVEX4:def3

      func ZeroCLC V -> C_Linear_Combination of V means

      : Def3: ( Carrier it ) = {} ;

      existence

      proof

        reconsider f = (the carrier of V --> 0c ) as Element of ( Funcs (the carrier of V, COMPLEX )) by FUNCT_2: 8;

        f is C_Linear_Combination of V

        proof

          take ( {} V);

          thus thesis by FUNCOP_1: 7;

        end;

        then

        reconsider f as C_Linear_Combination of V;

        take f;

        set C = { v where v be Element of V : (f . v) <> 0c };

        now

          set x = the Element of C;

          assume C <> {} ;

          then x in C;

          then ex v be Element of V st x = v & (f . v) <> 0c ;

          hence contradiction by FUNCOP_1: 7;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let L,L9 be C_Linear_Combination of V;

        assume

         A1: ( Carrier L) = {} & ( Carrier L9) = {} ;

        now

          let x be object;

          assume x in the carrier of V;

          then

          reconsider v = x as Element of V;

          

           A2: (L9 . v) <> 0c implies v in { u where u be Element of V : (L9 . u) <> 0c };

          (L . v) <> 0c implies v in { u where u be Element of V : (L . u) <> 0c };

          hence (L . x) = (L9 . x) by A1, A2;

        end;

        hence L = L9 by FUNCT_2: 12;

      end;

    end

    registration

      let V be non empty addLoopStr;

      cluster ( Carrier ( ZeroCLC V)) -> empty;

      coherence by Def3;

    end

    theorem :: CONVEX4:2

    

     Th2: for V be non empty addLoopStr, v be Element of V holds (( ZeroCLC V) . v) = 0c

    proof

      let V be non empty addLoopStr, v be Element of V;

      ( Carrier ( ZeroCLC V)) = {} & not v in {} ;

      hence thesis;

    end;

    definition

      let V be non empty addLoopStr;

      let A be Subset of V;

      :: CONVEX4:def4

      mode C_Linear_Combination of A -> C_Linear_Combination of V means

      : Def4: ( Carrier it ) c= A;

      existence

      proof

        take L = ( ZeroCLC V);

        thus thesis;

      end;

    end

    theorem :: CONVEX4:3

    for V be non empty addLoopStr, A,B be Subset of V, l be C_Linear_Combination of A st A c= B holds l is C_Linear_Combination of B

    proof

      let V be non empty addLoopStr;

      let A,B be Subset of V;

      let l be C_Linear_Combination of A;

      assume

       A1: A c= B;

      ( Carrier l) c= A by Def4;

      then ( Carrier l) c= B by A1;

      hence thesis by Def4;

    end;

    theorem :: CONVEX4:4

    

     Th4: for V be non empty addLoopStr, A be Subset of V holds ( ZeroCLC V) is C_Linear_Combination of A

    proof

      let V be non empty addLoopStr;

      let A be Subset of V;

      ( Carrier ( ZeroCLC V)) = {} & {} c= A;

      hence thesis by Def4;

    end;

    theorem :: CONVEX4:5

    

     Th5: for V be non empty addLoopStr, l be C_Linear_Combination of ( {} the carrier of V) holds l = ( ZeroCLC V)

    proof

      let V be non empty addLoopStr;

      let l be C_Linear_Combination of ( {} the carrier of V);

      ( Carrier l) c= {} by Def4;

      then ( Carrier l) = {} ;

      hence thesis by Def3;

    end;

    reserve x,y for set,

i for Nat;

    definition

      let V be non empty CLSStruct;

      let F be FinSequence of the carrier of V;

      let f be Function of the carrier of V, COMPLEX ;

      :: CONVEX4:def5

      func f (#) F -> FinSequence of the carrier of V means

      : Def5: ( len it ) = ( len F) & for i st i in ( dom it ) holds (it . i) = ((f . (F /. i)) * (F /. i));

      existence

      proof

        deffunc Q( set) = ((f . (F /. $1)) * (F /. $1));

        consider G be FinSequence such that

         A1: ( len G) = ( len F) and

         A2: for n be Nat st n in ( dom G) holds (G . n) = Q(n) from FINSEQ_1:sch 2;

        ( rng G) c= the carrier of V

        proof

          let x be object;

          assume x in ( rng G);

          then

          consider y be object such that

           A3: y in ( dom G) and

           A4: (G . y) = x by FUNCT_1:def 3;

          reconsider y as Element of NAT by A3;

          (G . y) = ((f . (F /. y)) * (F /. y)) by A2, A3;

          hence thesis by A4;

        end;

        then

        reconsider G as FinSequence of the carrier of V by FINSEQ_1:def 4;

        take G;

        thus thesis by A1, A2;

      end;

      uniqueness

      proof

        let H1,H2 be FinSequence of the carrier of V;

        assume that

         A5: ( len H1) = ( len F) and

         A6: for i st i in ( dom H1) holds (H1 . i) = ((f . (F /. i)) * (F /. i)) and

         A7: ( len H2) = ( len F) and

         A8: for i st i in ( dom H2) holds (H2 . i) = ((f . (F /. i)) * (F /. i));

        now

          let k be Nat;

          assume 1 <= k & k <= ( len H1);

          then

           A9: k in ( Seg ( len H1));

          then k in ( dom H1) by FINSEQ_1:def 3;

          then

           A10: (H1 . k) = ((f . (F /. k)) * (F /. k)) by A6;

          k in ( dom H2) by A5, A7, A9, FINSEQ_1:def 3;

          hence (H1 . k) = (H2 . k) by A8, A10;

        end;

        hence thesis by A5, A7, FINSEQ_1: 14;

      end;

    end

    reserve V for non empty CLSStruct,

u,v,v1,v2,v3 for VECTOR of V,

A for Subset of V,

l,l1,l2 for C_Linear_Combination of A,

x,y,y1,y2 for set,

a,b for Complex,

F for FinSequence of the carrier of V,

f for Function of the carrier of V, COMPLEX ;

    theorem :: CONVEX4:6

    

     Th6: x in ( dom F) & v = (F . x) implies ((f (#) F) . x) = ((f . v) * v)

    proof

      assume that

       A1: x in ( dom F) and

       A2: v = (F . x);

      

       A3: (F /. x) = (F . x) by A1, PARTFUN1:def 6;

      ( len (f (#) F)) = ( len F) by Def5;

      then x in ( dom (f (#) F)) by A1, FINSEQ_3: 29;

      hence thesis by A2, A3, Def5;

    end;

    theorem :: CONVEX4:7

    (f (#) ( <*> the carrier of V)) = ( <*> the carrier of V)

    proof

      ( len (f (#) ( <*> the carrier of V))) = ( len ( <*> the carrier of V)) by Def5

      .= 0 ;

      hence thesis;

    end;

    theorem :: CONVEX4:8

    

     Th8: (f (#) <*v*>) = <*((f . v) * v)*>

    proof

      

       A1: 1 in {1} by FINSEQ_1: 2;

      

       A2: ( len (f (#) <*v*>)) = ( len <*v*>) by Def5

      .= 1 by FINSEQ_1: 40;

      then ( dom (f (#) <*v*>)) = {1} by FINSEQ_1: 2, FINSEQ_1:def 3;

      

      then ((f (#) <*v*>) . 1) = ((f . ( <*v*> /. 1)) * ( <*v*> /. 1)) by A1, Def5

      .= ((f . ( <*v*> /. 1)) * v) by FINSEQ_4: 16

      .= ((f . v) * v) by FINSEQ_4: 16;

      hence thesis by A2, FINSEQ_1: 40;

    end;

    theorem :: CONVEX4:9

    

     Th9: (f (#) <*v1, v2*>) = <*((f . v1) * v1), ((f . v2) * v2)*>

    proof

      

       A1: ( len (f (#) <*v1, v2*>)) = ( len <*v1, v2*>) by Def5

      .= 2 by FINSEQ_1: 44;

      then

       A2: ( dom (f (#) <*v1, v2*>)) = {1, 2} by FINSEQ_1: 2, FINSEQ_1:def 3;

      2 in {1, 2} by FINSEQ_1: 2;

      

      then

       A3: ((f (#) <*v1, v2*>) . 2) = ((f . ( <*v1, v2*> /. 2)) * ( <*v1, v2*> /. 2)) by A2, Def5

      .= ((f . ( <*v1, v2*> /. 2)) * v2) by FINSEQ_4: 17

      .= ((f . v2) * v2) by FINSEQ_4: 17;

      1 in {1, 2} by FINSEQ_1: 2;

      

      then ((f (#) <*v1, v2*>) . 1) = ((f . ( <*v1, v2*> /. 1)) * ( <*v1, v2*> /. 1)) by A2, Def5

      .= ((f . ( <*v1, v2*> /. 1)) * v1) by FINSEQ_4: 17

      .= ((f . v1) * v1) by FINSEQ_4: 17;

      hence thesis by A1, A3, FINSEQ_1: 44;

    end;

    theorem :: CONVEX4:10

    

     Th10: (f (#) <*v1, v2, v3*>) = <*((f . v1) * v1), ((f . v2) * v2), ((f . v3) * v3)*>

    proof

      

       A1: ( len (f (#) <*v1, v2, v3*>)) = ( len <*v1, v2, v3*>) by Def5

      .= 3 by FINSEQ_1: 45;

      then

       A2: ( dom (f (#) <*v1, v2, v3*>)) = {1, 2, 3} by FINSEQ_1:def 3, FINSEQ_3: 1;

      3 in {1, 2, 3} by FINSEQ_3: 1;

      

      then

       A3: ((f (#) <*v1, v2, v3*>) . 3) = ((f . ( <*v1, v2, v3*> /. 3)) * ( <*v1, v2, v3*> /. 3)) by A2, Def5

      .= ((f . ( <*v1, v2, v3*> /. 3)) * v3) by FINSEQ_4: 18

      .= ((f . v3) * v3) by FINSEQ_4: 18;

      2 in {1, 2, 3} by FINSEQ_3: 1;

      

      then

       A4: ((f (#) <*v1, v2, v3*>) . 2) = ((f . ( <*v1, v2, v3*> /. 2)) * ( <*v1, v2, v3*> /. 2)) by A2, Def5

      .= ((f . ( <*v1, v2, v3*> /. 2)) * v2) by FINSEQ_4: 18

      .= ((f . v2) * v2) by FINSEQ_4: 18;

      1 in {1, 2, 3} by FINSEQ_3: 1;

      

      then ((f (#) <*v1, v2, v3*>) . 1) = ((f . ( <*v1, v2, v3*> /. 1)) * ( <*v1, v2, v3*> /. 1)) by A2, Def5

      .= ((f . ( <*v1, v2, v3*> /. 1)) * v1) by FINSEQ_4: 18

      .= ((f . v1) * v1) by FINSEQ_4: 18;

      hence thesis by A1, A4, A3, FINSEQ_1: 45;

    end;

    reserve K,L,L1,L2,L3 for C_Linear_Combination of V;

    definition

      let V be Abelian add-associative right_zeroed right_complementable non empty CLSStruct;

      let L be C_Linear_Combination of V;

      :: CONVEX4:def6

      func Sum L -> Element of V means

      : Def6: ex F be FinSequence of the carrier of V st F is one-to-one & ( rng F) = ( Carrier L) & it = ( Sum (L (#) F));

      existence

      proof

        consider F be FinSequence such that

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

         A2: F is one-to-one by FINSEQ_4: 58;

        reconsider F as FinSequence of the carrier of V by A1, FINSEQ_1:def 4;

        take ( Sum (L (#) F));

        take F;

        thus thesis by A1, A2;

      end;

      uniqueness

      proof

        let v1,v2 be Element of V;

        given F1 be FinSequence of the carrier of V such that

         A3: F1 is one-to-one and

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

         A5: v1 = ( Sum (L (#) F1));

        given F2 be FinSequence of the carrier of V such that

         A6: F2 is one-to-one and

         A7: ( rng F2) = ( Carrier L) and

         A8: v2 = ( Sum (L (#) F2));

        defpred P[ object, object] means {$2} = (F1 " {(F2 . $1)});

        

         A9: ( len F1) = ( len F2) by A3, A4, A6, A7, FINSEQ_1: 48;

        

         A10: ( dom F1) = ( Seg ( len F1)) by FINSEQ_1:def 3;

        

         A11: ( dom F2) = ( Seg ( len F2)) by FINSEQ_1:def 3;

        

         A12: for x be object st x in ( dom F1) holds ex y be object st y in ( dom F1) & P[x, y]

        proof

          let x be object;

          assume x in ( dom F1);

          then (F2 . x) in ( rng F1) by A4, A7, A9, A10, A11, FUNCT_1:def 3;

          then

          consider y be object such that

           A13: (F1 " {(F2 . x)}) = {y} by A3, FUNCT_1: 74;

          take y;

          y in (F1 " {(F2 . x)}) by A13, TARSKI:def 1;

          hence thesis by A13, FUNCT_1:def 7;

        end;

        consider f be Function of ( dom F1), ( dom F1) such that

         A14: for x be object st x in ( dom F1) holds P[x, (f . x)] from FUNCT_2:sch 1( A12);

        

         A15: ( rng f) = ( dom F1)

        proof

          thus ( rng f) c= ( dom F1) by RELAT_1:def 19;

          let y be object;

          assume

           A16: y in ( dom F1);

          then (F1 . y) in ( rng F2) by A4, A7, FUNCT_1:def 3;

          then

          consider x be object such that

           A17: x in ( dom F2) and

           A18: (F2 . x) = (F1 . y) by FUNCT_1:def 3;

          (F1 " {(F2 . x)}) = (F1 " ( Im (F1,y))) by A16, A18, FUNCT_1: 59;

          then (F1 " {(F2 . x)}) c= {y} by A3, FUNCT_1: 82;

          then {(f . x)} c= {y} by A9, A10, A11, A14, A17;

          then

           A19: (f . x) = y by ZFMISC_1: 18;

          x in ( dom f) by A9, A10, A11, A17, FUNCT_2:def 1;

          hence thesis by A19, FUNCT_1:def 3;

        end;

        set G1 = (L (#) F1);

        

         A20: ( len G1) = ( len F1) by Def5;

        

         A21: f is one-to-one

        proof

          let y1,y2 be object;

          assume that

           A22: y1 in ( dom f) and

           A23: y2 in ( dom f) and

           A24: (f . y1) = (f . y2);

          (F2 . y1) in ( rng F1) by A4, A7, A9, A10, A11, A22, FUNCT_1:def 3;

          then

           A25: {(F2 . y1)} c= ( rng F1) by ZFMISC_1: 31;

          (F2 . y2) in ( rng F1) by A4, A7, A9, A10, A11, A23, FUNCT_1:def 3;

          then

           A26: {(F2 . y2)} c= ( rng F1) by ZFMISC_1: 31;

          (F1 " {(F2 . y1)}) = {(f . y1)} & (F1 " {(F2 . y2)}) = {(f . y2)} by A14, A22, A23;

          then {(F2 . y1)} = {(F2 . y2)} by A24, A25, A26, FUNCT_1: 91;

          then (F2 . y1) = (F2 . y2) by ZFMISC_1: 3;

          hence thesis by A6, A9, A10, A11, A22, A23, FUNCT_1:def 4;

        end;

        set G2 = (L (#) F2);

        

         A27: ( dom G2) = ( Seg ( len G2)) by FINSEQ_1:def 3;

        reconsider f as Permutation of ( dom F1) by A15, A21, FUNCT_2: 57;

        ( dom F1) = ( Seg ( len F1)) & ( dom G1) = ( Seg ( len G1)) by FINSEQ_1:def 3;

        then

        reconsider f as Permutation of ( dom G1) by A20;

        

         A28: ( len G2) = ( len F2) by Def5;

        

         A29: ( dom G1) = ( Seg ( len G1)) by FINSEQ_1:def 3;

        now

          let i be Nat;

          assume

           A30: i in ( dom G2);

          then

           A31: (G2 . i) = ((L . (F2 /. i)) * (F2 /. i)) & (F2 . i) = (F2 /. i) by A28, A11, A27, Def5, PARTFUN1:def 6;

          i in ( dom f) by A9, A28, A10, A27, A30, FUNCT_2:def 1;

          then

           A32: (f . i) in ( dom F1) by A15, FUNCT_1:def 3;

          then

          reconsider m = (f . i) as Element of NAT ;

           {(F1 . (f . i))} = ( Im (F1,(f . i))) by A32, FUNCT_1: 59

          .= (F1 .: (F1 " {(F2 . i)})) by A9, A28, A10, A27, A14, A30;

          then

           A33: (F2 . i) = (F1 . m) by FUNCT_1: 75, ZFMISC_1: 18;

          (F1 . m) = (F1 /. m) by A32, PARTFUN1:def 6;

          hence (G2 . i) = (G1 . (f . i)) by A20, A10, A29, A32, A33, A31, Def5;

        end;

        hence thesis by A3, A4, A5, A6, A7, A8, A20, A28, FINSEQ_1: 48, RLVECT_2: 6;

      end;

    end

    theorem :: CONVEX4:11

    

     Th11: for V be Abelian add-associative right_zeroed right_complementable non empty CLSStruct holds ( Sum ( ZeroCLC V)) = ( 0. V)

    proof

      let V be Abelian add-associative right_zeroed right_complementable non empty CLSStruct;

      consider F be FinSequence of the carrier of V such that F is one-to-one and

       A1: ( rng F) = ( Carrier ( ZeroCLC V)) and

       A2: ( Sum ( ZeroCLC V)) = ( Sum (( ZeroCLC V) (#) F)) by Def6;

      F = {} by A1, RELAT_1: 41;

      then ( len (( ZeroCLC V) (#) F)) = 0 by Def5, CARD_1: 27;

      hence thesis by A2, RLVECT_1: 75;

    end;

    theorem :: CONVEX4:12

    for V be ComplexLinearSpace, A be Subset of V holds A <> {} implies (A is linearly-closed iff for l be C_Linear_Combination of A holds ( Sum l) in A)

    proof

      let V be ComplexLinearSpace;

      let A be Subset of V;

      assume

       A1: A <> {} ;

      thus A is linearly-closed implies for l be C_Linear_Combination of A holds ( Sum l) in A

      proof

        defpred P[ Nat] means for l be C_Linear_Combination of A st ( card ( Carrier l)) = $1 holds ( Sum l) in A;

        assume

         A2: A is linearly-closed;

        

         A3: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat;

          assume

           A4: P[k];

          hereby

            let l be C_Linear_Combination of A;

            deffunc F( Element of V) = (l . $1);

            consider F be FinSequence of the carrier of V such that

             A5: F is one-to-one and

             A6: ( rng F) = ( Carrier l) and

             A7: ( Sum l) = ( Sum (l (#) F)) by Def6;

            reconsider G = (F | ( Seg k)) as FinSequence of the carrier of V by FINSEQ_1: 18;

            assume

             A8: ( card ( Carrier l)) = (k + 1);

            then

             A9: ( len F) = (k + 1) by A5, A6, FINSEQ_4: 62;

            then

             A10: ( len (l (#) F)) = (k + 1) by Def5;

            (k + 1) in ( Seg (k + 1)) by FINSEQ_1: 4;

            then

             A11: (k + 1) in ( dom F) by A9, FINSEQ_1:def 3;

            then

            reconsider v = (F . (k + 1)) as VECTOR of V by FUNCT_1: 102;

            consider f be Function of the carrier of V, COMPLEX such that

             A12: (f . v) = 0c & for u be Element of V st u <> v holds (f . u) = F(u) from FUNCT_2:sch 6;

            reconsider f as Element of ( Funcs (the carrier of V, COMPLEX )) by FUNCT_2: 8;

            now

              let u be VECTOR of V;

              assume not u in ( Carrier l);

              then (l . u) = 0c ;

              hence (f . u) = 0c by A12;

            end;

            then

            reconsider f as C_Linear_Combination of V by Def1;

            

             A13: ( Carrier f) = (( Carrier l) \ {v})

            proof

              now

                let x be object;

                assume x in ( Carrier f);

                then

                 A14: ex u be VECTOR of V st u = x & (f . u) <> 0c ;

                then (f . x) = (l . x) by A12;

                then

                 A15: x in ( Carrier l) by A14;

                 not x in {v} by A12, A14, TARSKI:def 1;

                hence x in (( Carrier l) \ {v}) by A15, XBOOLE_0:def 5;

              end;

              hence ( Carrier f) c= (( Carrier l) \ {v});

              let x be object;

              assume

               A16: x in (( Carrier l) \ {v});

              then not x in {v} by XBOOLE_0:def 5;

              then x <> v by TARSKI:def 1;

              then

               A17: (l . x) = (f . x) by A12, A16;

              x in ( Carrier l) by A16, XBOOLE_0:def 5;

              then ex u be VECTOR of V st x = u & (l . u) <> 0c ;

              hence thesis by A17;

            end;

            

             A18: ( Carrier l) c= A by Def4;

            then ( Carrier f) c= (A \ {v}) by A13, XBOOLE_1: 33;

            then ( Carrier f) c= A by XBOOLE_1: 106;

            then

            reconsider f as C_Linear_Combination of A by Def4;

            

             A19: ( len G) = k by A9, FINSEQ_3: 53;

            then

             A20: ( len (f (#) G)) = k by Def5;

            

             A21: ( rng G) = ( Carrier f)

            proof

              thus ( rng G) c= ( Carrier f)

              proof

                let x be object;

                assume x in ( rng G);

                then

                consider y be object such that

                 A22: y in ( dom G) and

                 A23: (G . y) = x by FUNCT_1:def 3;

                reconsider y as Element of NAT by A22;

                

                 A24: ( dom G) c= ( dom F) & (G . y) = (F . y) by A22, FUNCT_1: 47, RELAT_1: 60;

                then x = v implies (k + 1) = y & y <= k & k < (k + 1) by A5, A19, A11, A22, A23, FINSEQ_3: 25, FUNCT_1:def 4, XREAL_1: 29;

                then

                 A25: not x in {v} by TARSKI:def 1;

                x in ( rng F) by A22, A23, A24, FUNCT_1:def 3;

                hence thesis by A6, A13, A25, XBOOLE_0:def 5;

              end;

              let x be object;

              assume

               A26: x in ( Carrier f);

              then x in ( rng F) by A6, A13, XBOOLE_0:def 5;

              then

              consider y be object such that

               A27: y in ( dom F) and

               A28: (F . y) = x by FUNCT_1:def 3;

              now

                assume not y in ( Seg k);

                then y in (( dom F) \ ( Seg k)) by A27, XBOOLE_0:def 5;

                then y in (( Seg (k + 1)) \ ( Seg k)) by A9, FINSEQ_1:def 3;

                then y in {(k + 1)} by FINSEQ_3: 15;

                then y = (k + 1) by TARSKI:def 1;

                then not v in {v} by A13, A26, A28, XBOOLE_0:def 5;

                hence contradiction by TARSKI:def 1;

              end;

              then y in (( dom F) /\ ( Seg k)) by A27, XBOOLE_0:def 4;

              then

               A29: y in ( dom G) by RELAT_1: 61;

              then (G . y) = (F . y) by FUNCT_1: 47;

              hence thesis by A28, A29, FUNCT_1:def 3;

            end;

            (( Seg (k + 1)) /\ ( Seg k)) = ( Seg k) by FINSEQ_1: 7, NAT_1: 12

            .= ( dom (f (#) G)) by A20, FINSEQ_1:def 3;

            then

             A30: ( dom (f (#) G)) = (( dom (l (#) F)) /\ ( Seg k)) by A10, FINSEQ_1:def 3;

            now

              let x be object;

              assume

               A31: x in ( dom (f (#) G));

              then

               A32: x in ( dom G) by A19, A20, FINSEQ_3: 29;

              then

               A33: (G . x) in ( rng G) by FUNCT_1:def 3;

              then

              reconsider u = (G . x) as VECTOR of V;

              

               A34: (F . x) = u by A32, FUNCT_1: 47;

               not u in {v} by A13, A21, A33, XBOOLE_0:def 5;

              then

               A35: u <> v by TARSKI:def 1;

              x in ( dom (l (#) F)) by A30, A31, XBOOLE_0:def 4;

              then

               A36: x in ( dom F) by A9, A10, FINSEQ_3: 29;

              ((f (#) G) . x) = ((f . u) * u) by A32, Th6

              .= ((l . u) * u) by A12, A35;

              hence ((f (#) G) . x) = ((l (#) F) . x) by A36, A34, Th6;

            end;

            then

             A37: (f (#) G) = ((l (#) F) | ( Seg k)) by A30, FUNCT_1: 46;

            v in ( rng F) by A11, FUNCT_1:def 3;

            then {v} c= ( Carrier l) by A6, ZFMISC_1: 31;

            then ( card ( Carrier f)) = ((k + 1) - ( card {v})) by A8, A13, CARD_2: 44;

            then ( card ( Carrier f)) = ((k + 1) - 1) by CARD_1: 30;

            then

             A38: ( Sum f) in A by A4;

            v in ( Carrier l) by A6, A11, FUNCT_1:def 3;

            then

             A39: ((l . v) * v) in A by A2, A18;

            G is one-to-one by A5, FUNCT_1: 52;

            then

             A40: ( Sum (f (#) G)) = ( Sum f) by A21, Def6;

            ( dom (f (#) G)) = ( Seg ( len (f (#) G))) & ((l (#) F) . ( len F)) = ((l . v) * v) by A9, A11, Th6, FINSEQ_1:def 3;

            then ( Sum (l (#) F)) = (( Sum (f (#) G)) + ((l . v) * v)) by A9, A10, A20, A37, RLVECT_1: 38;

            hence ( Sum l) in A by A2, A7, A39, A40, A38;

          end;

        end;

        let l be C_Linear_Combination of A;

        

         A41: ( card ( Carrier l)) = ( card ( Carrier l));

        now

          let l be C_Linear_Combination of A;

          assume ( card ( Carrier l)) = 0 ;

          then ( Carrier l) = {} ;

          then l = ( ZeroCLC V) by Def3;

          then ( Sum l) = ( 0. V) by Th11;

          hence ( Sum l) in A by A1, A2, CLVECT_1: 20;

        end;

        then

         A42: P[ 0 ];

        for k be Nat holds P[k] from NAT_1:sch 2( A42, A3);

        hence thesis by A41;

      end;

      assume

       A43: for l be C_Linear_Combination of A holds ( Sum l) in A;

      ( ZeroCLC V) is C_Linear_Combination of A & ( Sum ( ZeroCLC V)) = ( 0. V) by Th4, Th11;

      then

       A44: ( 0. V) in A by A43;

      

       A45: for a be Complex, v be VECTOR of V st v in A holds (a * v) in A

      proof

        let a be Complex, v be VECTOR of V;

        assume

         A46: v in A;

        now

          reconsider a1 = a as Element of COMPLEX by XCMPLX_0:def 2;

          deffunc F( Element of V) = 0c ;

          consider f be Function of the carrier of V, COMPLEX such that

           A47: (f . v) = a1 & for u be Element of V st u <> v holds (f . u) = F(u) from FUNCT_2:sch 6;

          reconsider f as Element of ( Funcs (the carrier of V, COMPLEX )) by FUNCT_2: 8;

          now

            let u be VECTOR of V;

            assume not u in {v};

            then u <> v by TARSKI:def 1;

            hence (f . u) = 0 by A47;

          end;

          then

          reconsider f as C_Linear_Combination of V by Def1;

          assume

           A48: a <> 0 ;

          

           A49: ( Carrier f) = {v}

          proof

            now

              let x be object;

              assume x in ( Carrier f);

              then ex u be VECTOR of V st x = u & (f . u) <> 0 ;

              then x = v by A47;

              hence x in {v} by TARSKI:def 1;

            end;

            hence ( Carrier f) c= {v};

            let x be object;

            assume x in {v};

            then x = v by TARSKI:def 1;

            hence thesis by A48, A47;

          end;

           {v} c= A by A46, ZFMISC_1: 31;

          then

          reconsider f as C_Linear_Combination of A by A49, Def4;

          consider F be FinSequence of the carrier of V such that

           A50: F is one-to-one & ( rng F) = ( Carrier f) and

           A51: ( Sum (f (#) F)) = ( Sum f) by Def6;

          F = <*v*> by A49, A50, FINSEQ_3: 97;

          then (f (#) F) = <*((f . v) * v)*> by Th8;

          then ( Sum f) = (a * v) by A47, A51, RLVECT_1: 44;

          hence thesis by A43;

        end;

        hence thesis by A44, CLVECT_1: 1;

      end;

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

      proof

        let v,u be VECTOR of V;

        assume that

         A52: v in A and

         A53: u in A;

        

         A54: ( 1r * v) = v by CLVECT_1:def 5;

        

         A55: ( 1r * u) = u by CLVECT_1:def 5;

         A56:

        now

          deffunc F( Element of V) = 0c ;

          assume

           A57: v <> u;

          consider f be Function of the carrier of V, COMPLEX such that

           A58: (f . v) = 1r & (f . u) = 1r and

           A59: for w be Element of V st w <> v & w <> u holds (f . w) = F(w) from FUNCT_2:sch 7( A57);

          reconsider f as Element of ( Funcs (the carrier of V, COMPLEX )) by FUNCT_2: 8;

          now

            let w be VECTOR of V;

            assume not w in {v, u};

            then w <> v & w <> u by TARSKI:def 2;

            hence (f . w) = 0 by A59;

          end;

          then

          reconsider f as C_Linear_Combination of V by Def1;

          

           A60: ( Carrier f) = {v, u}

          proof

            thus ( Carrier f) c= {v, u}

            proof

              let x be object;

              assume x in ( Carrier f);

              then ex w be VECTOR of V st x = w & (f . w) <> 0c ;

              then x = v or x = u by A59;

              hence thesis by TARSKI:def 2;

            end;

            let x be object;

            assume x in {v, u};

            then x = v or x = u by TARSKI:def 2;

            hence thesis by A58;

          end;

          then ( Carrier f) c= A by A52, A53, ZFMISC_1: 32;

          then

          reconsider f as C_Linear_Combination of A by Def4;

          consider F be FinSequence of the carrier of V such that

           A61: F is one-to-one & ( rng F) = ( Carrier f) and

           A62: ( Sum (f (#) F)) = ( Sum f) by Def6;

          F = <*v, u*> or F = <*u, v*> by A57, A60, A61, FINSEQ_3: 99;

          then (f (#) F) = <*( 1r * v), ( 1r * u)*> or (f (#) F) = <*( 1r * u), ( 1r * v)*> by A58, Th9;

          then ( Sum f) = (v + u) by A55, A54, A62, RLVECT_1: 45;

          hence thesis by A43;

        end;

        (v + v) = (( 1r + 1r ) * v) by A54, CLVECT_1:def 3;

        hence thesis by A45, A52, A56;

      end;

      hence thesis by A45;

    end;

    theorem :: CONVEX4:13

    for V be Abelian add-associative right_zeroed right_complementable non empty CLSStruct, l be C_Linear_Combination of ( {} the carrier of V) holds ( Sum l) = ( 0. V)

    proof

      let V be Abelian add-associative right_zeroed right_complementable non empty CLSStruct;

      let l be C_Linear_Combination of ( {} the carrier of V);

      l = ( ZeroCLC V) by Th5;

      hence thesis by Th11;

    end;

    theorem :: CONVEX4:14

    

     Th14: for V be ComplexLinearSpace, v be VECTOR of V, l be C_Linear_Combination of {v} holds ( Sum l) = ((l . v) * v)

    proof

      let V be ComplexLinearSpace;

      let v be VECTOR of V;

      let l be C_Linear_Combination of {v};

      

       A1: ( Carrier l) c= {v} by Def4;

      per cases by A1, ZFMISC_1: 33;

        suppose ( Carrier l) = {} ;

        then

         A2: l = ( ZeroCLC V) by Def3;

        

        hence ( Sum l) = ( 0. V) by Th11

        .= ( 0c * v) by CLVECT_1: 1

        .= ((l . v) * v) by A2, Th2;

      end;

        suppose ( Carrier l) = {v};

        then

        consider F be FinSequence of the carrier of V such that

         A3: F is one-to-one & ( rng F) = {v} and

         A4: ( Sum l) = ( Sum (l (#) F)) by Def6;

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

        then (l (#) F) = <*((l . v) * v)*> by Th8;

        hence thesis by A4, RLVECT_1: 44;

      end;

    end;

    theorem :: CONVEX4:15

    

     Th15: for V be ComplexLinearSpace, v1,v2 be VECTOR of V holds v1 <> v2 implies for l be C_Linear_Combination of {v1, v2} holds ( Sum l) = (((l . v1) * v1) + ((l . v2) * v2))

    proof

      let V be ComplexLinearSpace;

      let v1,v2 be VECTOR of V;

      assume

       A1: v1 <> v2;

      let l be C_Linear_Combination of {v1, v2};

      

       A2: ( 0. V) = ( 0c * v1) by CLVECT_1: 1;

      

       A3: ( Carrier l) c= {v1, v2} by Def4;

      

       A4: ( 0. V) = ( 0c * v2) by CLVECT_1: 1;

      per cases by A3, ZFMISC_1: 36;

        suppose ( Carrier l) = {} ;

        then

         A5: l = ( ZeroCLC V) by Def3;

        

        hence ( Sum l) = ( 0. V) by Th11

        .= (( 0. V) + ( 0. V))

        .= (((l . v1) * v1) + ( 0c * v2)) by A4, A5, Th2, CLVECT_1: 1

        .= (((l . v1) * v1) + ((l . v2) * v2)) by A5, Th2;

      end;

        suppose

         A6: ( Carrier l) = {v1};

        then

        reconsider L = l as C_Linear_Combination of {v1} by Def4;

        ( Sum L) = ((l . v1) * v1) by Th14;

        then

         A7: ( Sum l) = (((l . v1) * v1) + ( 0. V));

         not v2 in ( Carrier l) by A1, A6, TARSKI:def 1;

        hence thesis by A4, A7;

      end;

        suppose

         A8: ( Carrier l) = {v2};

        then

        reconsider L = l as C_Linear_Combination of {v2} by Def4;

        ( Sum L) = ((l . v2) * v2) by Th14;

        then

         A9: ( Sum l) = (( 0. V) + ((l . v2) * v2));

         not v1 in ( Carrier l) by A1, A8, TARSKI:def 1;

        hence thesis by A2, A9;

      end;

        suppose ( Carrier l) = {v1, v2};

        then

        consider F be FinSequence of the carrier of V such that

         A10: F is one-to-one & ( rng F) = {v1, v2} and

         A11: ( Sum l) = ( Sum (l (#) F)) by Def6;

        F = <*v1, v2*> or F = <*v2, v1*> by A1, A10, FINSEQ_3: 99;

        then (l (#) F) = <*((l . v1) * v1), ((l . v2) * v2)*> or (l (#) F) = <*((l . v2) * v2), ((l . v1) * v1)*> by Th9;

        hence thesis by A11, RLVECT_1: 45;

      end;

    end;

    theorem :: CONVEX4:16

    for V be Abelian add-associative right_zeroed right_complementable non empty CLSStruct, L be C_Linear_Combination of V holds ( Carrier L) = {} implies ( Sum L) = ( 0. V)

    proof

      let V be Abelian add-associative right_zeroed right_complementable non empty CLSStruct;

      let L be C_Linear_Combination of V;

      assume ( Carrier L) = {} ;

      then L = ( ZeroCLC V) by Def3;

      hence thesis by Th11;

    end;

    theorem :: CONVEX4:17

    for V be ComplexLinearSpace, L be C_Linear_Combination of V, v be VECTOR of V holds ( Carrier L) = {v} implies ( Sum L) = ((L . v) * v)

    proof

      let V be ComplexLinearSpace;

      let L be C_Linear_Combination of V;

      let v be VECTOR of V;

      assume ( Carrier L) = {v};

      then L is C_Linear_Combination of {v} by Def4;

      hence thesis by Th14;

    end;

    theorem :: CONVEX4:18

    

     Th18: for V be ComplexLinearSpace, L be C_Linear_Combination of V, v1,v2 be VECTOR of V holds ( Carrier L) = {v1, v2} & v1 <> v2 implies ( Sum L) = (((L . v1) * v1) + ((L . v2) * v2))

    proof

      let V be ComplexLinearSpace;

      let L be C_Linear_Combination of V;

      let v1,v2 be VECTOR of V;

      assume that

       A1: ( Carrier L) = {v1, v2} and

       A2: v1 <> v2;

      L is C_Linear_Combination of {v1, v2} by A1, Def4;

      hence thesis by A2, Th15;

    end;

    definition

      let V be non empty addLoopStr;

      let L1,L2 be C_Linear_Combination of V;

      :: original: =

      redefine

      :: CONVEX4:def7

      pred L1 = L2 means for v be Element of V holds (L1 . v) = (L2 . v);

      compatibility by FUNCT_2: 63;

    end

    definition

      let V be non empty addLoopStr;

      let L1,L2 be C_Linear_Combination of V;

      :: original: +

      redefine

      :: CONVEX4:def8

      func L1 + L2 -> C_Linear_Combination of V means

      : Def8: for v be Element of V holds (it . v) = ((L1 . v) + (L2 . v));

      coherence

      proof

        reconsider f = (L1 + L2) as Element of ( Funcs (the carrier of V, COMPLEX )) by FUNCT_2: 8;

        now

          let v be Element of V;

          assume

           A1: not v in (( Carrier L1) \/ ( Carrier L2));

          then not v in ( Carrier L2) by XBOOLE_0:def 3;

          then

           A2: (L2 . v) = 0 ;

           not v in ( Carrier L1) by A1, XBOOLE_0:def 3;

          then (L1 . v) = 0 ;

          

          hence (f . v) = ( 0 + 0 ) by A2, VALUED_1: 1

          .= 0 ;

        end;

        hence thesis by Def1;

      end;

      compatibility

      proof

        let f be C_Linear_Combination of V;

        thus f = (L1 + L2) implies for v be Element of V holds (f . v) = ((L1 . v) + (L2 . v)) by VALUED_1: 1;

        assume for v be Element of V holds (f . v) = ((L1 . v) + (L2 . v));

        then

         A3: for c be object st c in ( dom f) holds (f . c) = ((L1 . c) + (L2 . c));

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

        then ( dom f) = (( dom L1) /\ ( dom L2)) by FUNCT_2: 92;

        hence f = (L1 + L2) by A3, VALUED_1:def 1;

      end;

    end

    theorem :: CONVEX4:19

    

     Th19: ( Carrier (L1 + L2)) c= (( Carrier L1) \/ ( Carrier L2))

    proof

      let x be object;

      assume x in ( Carrier (L1 + L2));

      then

      consider u such that

       A1: x = u and

       A2: ((L1 + L2) . u) <> 0c ;

      ((L1 + L2) . u) = ((L1 . u) + (L2 . u)) by Def8;

      then (L1 . u) <> 0c or (L2 . u) <> 0c by A2;

      then x in ( Carrier L1) or x in ( Carrier L2) by A1;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: CONVEX4:20

    

     Th20: L1 is C_Linear_Combination of A & L2 is C_Linear_Combination of A implies (L1 + L2) is C_Linear_Combination of A

    proof

      assume L1 is C_Linear_Combination of A & L2 is C_Linear_Combination of A;

      then ( Carrier L1) c= A & ( Carrier L2) c= A by Def4;

      then

       A1: (( Carrier L1) \/ ( Carrier L2)) c= A by XBOOLE_1: 8;

      ( Carrier (L1 + L2)) c= (( Carrier L1) \/ ( Carrier L2)) by Th19;

      hence ( Carrier (L1 + L2)) c= A by A1;

    end;

    definition

      let V, A;

      let L1,L2 be C_Linear_Combination of A;

      :: original: +

      redefine

      func L1 + L2 -> C_Linear_Combination of A ;

      coherence by Th20;

    end

    theorem :: CONVEX4:21

    for V be non empty addLoopStr, L1,L2 be C_Linear_Combination of V holds (L1 + L2) = (L2 + L1);

    theorem :: CONVEX4:22

    

     Th22: (L1 + (L2 + L3)) = ((L1 + L2) + L3)

    proof

      let v;

      

      thus ((L1 + (L2 + L3)) . v) = ((L1 . v) + ((L2 + L3) . v)) by Def8

      .= ((L1 . v) + ((L2 . v) + (L3 . v))) by Def8

      .= (((L1 . v) + (L2 . v)) + (L3 . v))

      .= (((L1 + L2) . v) + (L3 . v)) by Def8

      .= (((L1 + L2) + L3) . v) by Def8;

    end;

    theorem :: CONVEX4:23

    

     Th23: (L + ( ZeroCLC V)) = L

    proof

      let v;

      

      thus ((L + ( ZeroCLC V)) . v) = ((L . v) + (( ZeroCLC V) . v)) by Def8

      .= ((L . v) + 0c ) by Th2

      .= (L . v);

    end;

    definition

      let V;

      let a be Complex;

      let L;

      :: CONVEX4:def9

      func a * L -> C_Linear_Combination of V means

      : Def9: for v holds (it . v) = (a * (L . v));

      existence

      proof

        reconsider a as Element of COMPLEX by XCMPLX_0:def 2;

        deffunc F( Element of V) = ( In ((a * (L . $1)), COMPLEX ));

        consider f be Function of the carrier of V, COMPLEX such that

         A1: for v be Element of V holds (f . v) = F(v) from FUNCT_2:sch 4;

        reconsider f as Element of ( Funcs (the carrier of V, COMPLEX )) by FUNCT_2: 8;

        now

          let v;

          assume not v in ( Carrier L);

          then

           A2: (L . v) = 0c ;

          

          thus (f . v) = F(v) by A1

          .= 0c by A2;

        end;

        then

        reconsider f as C_Linear_Combination of V by Def1;

        take f;

        let v;

        (f . v) = F(v) by A1;

        hence thesis;

      end;

      uniqueness

      proof

        let L1, L2;

        assume

         A3: for v holds (L1 . v) = (a * (L . v));

        assume

         A4: for v holds (L2 . v) = (a * (L . v));

        let v;

        

        thus (L1 . v) = (a * (L . v)) by A3

        .= (L2 . v) by A4;

      end;

    end

    theorem :: CONVEX4:24

    

     Th24: a <> 0c implies ( Carrier (a * L)) = ( Carrier L)

    proof

      set T = { u : ((a * L) . u) <> 0c };

      set S = { v : (L . v) <> 0c };

      assume

       A1: a <> 0c ;

      T = S

      proof

        thus T c= S

        proof

          let x be object;

          assume x in T;

          then

          consider u such that

           A2: x = u and

           A3: ((a * L) . u) <> 0c ;

          ((a * L) . u) = (a * (L . u)) by Def9;

          then (L . u) <> 0c by A3;

          hence thesis by A2;

        end;

        let x be object;

        assume x in S;

        then

        consider v such that

         A4: x = v & (L . v) <> 0c ;

        ((a * L) . v) = (a * (L . v)) by Def9;

        hence thesis by A1, A4;

      end;

      hence thesis;

    end;

    theorem :: CONVEX4:25

    

     Th25: ( 0c * L) = ( ZeroCLC V)

    proof

      let v;

      

      thus (( 0c * L) . v) = ( 0c * (L . v)) by Def9

      .= (( ZeroCLC V) . v) by Th2;

    end;

    theorem :: CONVEX4:26

    

     Th26: L is C_Linear_Combination of A implies (a * L) is C_Linear_Combination of A

    proof

      assume

       A1: L is C_Linear_Combination of A;

       A2:

      now

        assume a <> 0c ;

        then ( Carrier (a * L)) = ( Carrier L) by Th24;

        hence thesis by A1, Def4;

      end;

      a = 0c implies (a * L) = ( ZeroCLC V) by Th25;

      hence thesis by A2, Th4;

    end;

    theorem :: CONVEX4:27

    

     Th27: ((a + b) * L) = ((a * L) + (b * L))

    proof

      let v;

      

      thus (((a + b) * L) . v) = ((a + b) * (L . v)) by Def9

      .= ((a * (L . v)) + (b * (L . v)))

      .= (((a * L) . v) + (b * (L . v))) by Def9

      .= (((a * L) . v) + ((b * L) . v)) by Def9

      .= (((a * L) + (b * L)) . v) by Def8;

    end;

    theorem :: CONVEX4:28

    

     Th28: (a * (L1 + L2)) = ((a * L1) + (a * L2))

    proof

      let v;

      

      thus ((a * (L1 + L2)) . v) = (a * ((L1 + L2) . v)) by Def9

      .= (a * ((L1 . v) + (L2 . v))) by Def8

      .= ((a * (L1 . v)) + (a * (L2 . v)))

      .= (((a * L1) . v) + (a * (L2 . v))) by Def9

      .= (((a * L1) . v) + ((a * L2) . v)) by Def9

      .= (((a * L1) + (a * L2)) . v) by Def8;

    end;

    theorem :: CONVEX4:29

    

     Th29: (a * (b * L)) = ((a * b) * L)

    proof

      let v;

      

      thus ((a * (b * L)) . v) = (a * ((b * L) . v)) by Def9

      .= (a * (b * (L . v))) by Def9

      .= ((a * b) * (L . v))

      .= (((a * b) * L) . v) by Def9;

    end;

    theorem :: CONVEX4:30

    

     Th30: ( 1r * L) = L

    proof

      let v;

      

      thus (( 1r * L) . v) = ( 1r * (L . v)) by Def9

      .= (L . v);

    end;

    definition

      let V, L;

      :: CONVEX4:def10

      func - L -> C_Linear_Combination of V equals (( - 1r ) * L);

      correctness ;

    end

    theorem :: CONVEX4:31

    

     Th31: (( - L) . v) = ( - (L . v))

    proof

      

      thus (( - L) . v) = (( - 1r ) * (L . v)) by Def9

      .= ( - (L . v));

    end;

    theorem :: CONVEX4:32

    (L1 + L2) = ( ZeroCLC V) implies L2 = ( - L1)

    proof

      assume

       A1: (L1 + L2) = ( ZeroCLC V);

      let v;

      ((L1 . v) + (L2 . v)) = (( ZeroCLC V) . v) by A1, Def8

      .= 0c by Th2;

      

      hence (L2 . v) = ( - (L1 . v))

      .= (( - L1) . v) by Th31;

    end;

    theorem :: CONVEX4:33

    ( - ( - L)) = L

    proof

      let v;

      

      thus (( - ( - L)) . v) = (((( - 1r ) * ( - 1r )) * L) . v) by Th29

      .= ( 1r * (L . v)) by Def9

      .= (L . v);

    end;

    definition

      let V;

      let L1, L2;

      :: CONVEX4:def11

      func L1 - L2 -> C_Linear_Combination of V equals (L1 + ( - L2));

      correctness ;

    end

    theorem :: CONVEX4:34

    

     Th34: ((L1 - L2) . v) = ((L1 . v) - (L2 . v))

    proof

      

      thus ((L1 - L2) . v) = ((L1 . v) + (( - L2) . v)) by Def8

      .= ((L1 . v) - (L2 . v)) by Th31;

    end;

    theorem :: CONVEX4:35

    ( Carrier (L1 - L2)) c= (( Carrier L1) \/ ( Carrier L2))

    proof

      ( Carrier (L1 - L2)) c= (( Carrier L1) \/ ( Carrier ( - L2))) by Th19;

      hence thesis by Th24;

    end;

    theorem :: CONVEX4:36

    L1 is C_Linear_Combination of A & L2 is C_Linear_Combination of A implies (L1 - L2) is C_Linear_Combination of A

    proof

      assume that

       A1: L1 is C_Linear_Combination of A and

       A2: L2 is C_Linear_Combination of A;

      ( - L2) is C_Linear_Combination of A by A2, Th26;

      hence thesis by A1, Th20;

    end;

    theorem :: CONVEX4:37

    

     Th37: (L - L) = ( ZeroCLC V)

    proof

      let v;

      

      thus ((L - L) . v) = ((L . v) - (L . v)) by Th34

      .= (( ZeroCLC V) . v) by Th2;

    end;

    definition

      let V;

      :: CONVEX4:def12

      func C_LinComb V -> set means

      : Def12: x in it iff x is C_Linear_Combination of V;

      existence

      proof

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

        consider A be set such that

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

        take A;

        let x;

        thus x in A implies x is C_Linear_Combination of V by A1;

        assume x is C_Linear_Combination of V;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let D1,D2 be set;

        assume

         A2: for x holds x in D1 iff x is C_Linear_Combination of V;

        assume

         A3: for x holds x in D2 iff x is C_Linear_Combination of V;

        thus D1 c= D2

        proof

          let x be object;

          assume x in D1;

          then x is C_Linear_Combination of V by A2;

          hence thesis by A3;

        end;

        let x be object;

        assume x in D2;

        then x is C_Linear_Combination of V by A3;

        hence thesis by A2;

      end;

    end

    registration

      let V;

      cluster ( C_LinComb V) -> non empty;

      coherence

      proof

        set x = the C_Linear_Combination of V;

        x in ( C_LinComb V) by Def12;

        hence thesis;

      end;

    end

    reserve e,e1,e2 for Element of ( C_LinComb V);

    definition

      let V;

      let e;

      :: CONVEX4:def13

      func @ e -> C_Linear_Combination of V equals e;

      coherence by Def12;

    end

    definition

      let V;

      let L;

      :: CONVEX4:def14

      func @ L -> Element of ( C_LinComb V) equals L;

      coherence by Def12;

    end

    definition

      let V;

      :: CONVEX4:def15

      func C_LCAdd V -> BinOp of ( C_LinComb V) means

      : Def15: for e1, e2 holds (it . (e1,e2)) = (( @ e1) + ( @ e2));

      existence

      proof

        deffunc F( Element of ( C_LinComb V), Element of ( C_LinComb V)) = ( @ (( @ $1) + ( @ $2)));

        consider o be BinOp of ( C_LinComb V) such that

         A1: for e1, e2 holds (o . (e1,e2)) = F(e1,e2) from BINOP_1:sch 4;

        take o;

        let e1, e2;

        

        thus (o . (e1,e2)) = ( @ (( @ e1) + ( @ e2))) by A1

        .= (( @ e1) + ( @ e2));

      end;

      uniqueness

      proof

        let o1,o2 be BinOp of ( C_LinComb V);

        assume

         A2: for e1, e2 holds (o1 . (e1,e2)) = (( @ e1) + ( @ e2));

        assume

         A3: for e1, e2 holds (o2 . (e1,e2)) = (( @ e1) + ( @ e2));

        now

          let e1, e2;

          

          thus (o1 . (e1,e2)) = (( @ e1) + ( @ e2)) by A2

          .= (o2 . (e1,e2)) by A3;

        end;

        hence thesis;

      end;

    end

    definition

      let V;

      :: CONVEX4:def16

      func C_LCMult V -> Function of [: COMPLEX , ( C_LinComb V):], ( C_LinComb V) means

      : Def16: for a, e holds (it . [a, e]) = (a * ( @ e));

      existence

      proof

        defpred P[ Element of COMPLEX , Element of ( C_LinComb V), set] means ex a st a = $1 & $3 = (a * ( @ $2));

        

         A1: for x be Element of COMPLEX , e1 holds ex e2 st P[x, e1, e2]

        proof

          let x be Element of COMPLEX , e1;

          take ( @ (x * ( @ e1)));

          take x;

          thus thesis;

        end;

        consider g be Function of [: COMPLEX , ( C_LinComb V):], ( C_LinComb V) such that

         A2: for x be Element of COMPLEX , e holds P[x, e, (g . (x,e))] from BINOP_1:sch 3( A1);

        take g;

        let a, e;

        a in COMPLEX by XCMPLX_0:def 2;

        then ex b st b = a & (g . (a,e)) = (b * ( @ e)) by A2;

        hence thesis;

      end;

      uniqueness

      proof

        let g1,g2 be Function of [: COMPLEX , ( C_LinComb V):], ( C_LinComb V);

        assume

         A3: for a, e holds (g1 . [a, e]) = (a * ( @ e));

        assume

         A4: for a, e holds (g2 . [a, e]) = (a * ( @ e));

        now

          let x be Element of COMPLEX , e;

          

          thus (g1 . (x,e)) = (x * ( @ e)) by A3

          .= (g2 . (x,e)) by A4;

        end;

        hence thesis;

      end;

    end

    definition

      let V;

      :: CONVEX4:def17

      func LC_CLSpace V -> ComplexLinearSpace equals CLSStruct (# ( C_LinComb V), ( @ ( ZeroCLC V)), ( C_LCAdd V), ( C_LCMult V) #);

      coherence

      proof

        set S = CLSStruct (# ( C_LinComb V), ( @ ( ZeroCLC V)), ( C_LCAdd V), ( C_LCMult V) #);

         A1:

        now

          let a,b be Complex, v,u,w be VECTOR of S;

          reconsider a1 = a, b1 = b as Element of COMPLEX by XCMPLX_0:def 2;

          reconsider x = v, y = u, z = w, yx = (u + v), xz = (v + w), ax = (a1 * v), az = (a1 * w), bx = (b1 * v) as Element of ( C_LinComb V);

          

           A2: ( @ z) = w & ( @ yx) = (u + v);

          

           A3: ( @ xz) = (v + w) & ( @ ax) = (a * v);

          

           A4: ( @ az) = (a * w) & ( @ bx) = (b * v);

          ( @ x) = v & ( @ y) = u;

          then

          reconsider K = v, L = u, M = w, LK = (u + v), KM = (v + w), aK = (a * v), aM = (a * w), bK = (b * v) as C_Linear_Combination of V by A2, A3, A4;

           A5:

          now

            let v,u be VECTOR of S, K, L;

            

             A6: ( @ ( @ K)) = K & ( @ ( @ L)) = L;

            assume v = K & u = L;

            hence (v + u) = (K + L) by A6, Def15;

          end;

          

          hence (v + w) = (K + M)

          .= (w + v) by A5;

          

          thus ((u + v) + w) = (LK + M) by A5

          .= ((L + K) + M) by A5

          .= (L + (K + M)) by Th22

          .= (L + KM) by A5

          .= (u + (v + w)) by A5;

          

          thus (v + ( 0. S)) = (K + ( ZeroCLC V)) by A5

          .= v by Th23;

          ( - K) in the carrier of S by Def12;

          then ( - K) in S;

          then ( - K) = ( vector (S,( - K))) by RLVECT_2:def 1;

          

          then (v + ( vector (S,( - K)))) = (K - K) by A5

          .= ( 0. S) by Th37;

          hence ex w be VECTOR of S st (v + w) = ( 0. S);

           A7:

          now

            let v be VECTOR of S, L;

            let a be Complex;

            assume v = L;

            then (( C_LCMult V) . [a, v]) = (a * ( @ ( @ L))) by Def16;

            hence (a * v) = (a * L);

          end;

          

          hence (a * (v + w)) = (a1 * KM)

          .= (a1 * (K + M)) by A5

          .= ((a1 * K) + (a1 * M)) by Th28

          .= (aK + (a1 * M)) by A7

          .= (aK + aM) by A7

          .= ((a * v) + (a * w)) by A5;

          

          thus ((a + b) * v) = ((a1 + b1) * K) by A7

          .= ((a1 * K) + (b1 * K)) by Th27

          .= (aK + (b * K)) by A7

          .= (aK + bK) by A7

          .= ((a * v) + (b * v)) by A5;

          

          thus ((a * b) * v) = ((a * b) * K) by A7

          .= (a1 * (b1 * K)) by Th29

          .= (a * bK) by A7

          .= (a * (b * v)) by A7;

          

          thus ( 1r * v) = ( 1r * K) by A7

          .= v by Th30;

        end;

        

         A8: for v be Element of S holds v is right_complementable by A1;

        for u,v,w be VECTOR of S holds ((u + v) + w) = (u + (v + w)) by A1;

        hence thesis by A1, A8, ALGSTR_0:def 16, CLVECT_1:def 2, CLVECT_1:def 3, CLVECT_1:def 4, CLVECT_1:def 5, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4;

      end;

    end

    registration

      let V;

      cluster ( LC_CLSpace V) -> strict non empty;

      coherence ;

    end

    theorem :: CONVEX4:38

    

     Th38: (( vector (( LC_CLSpace V),L1)) + ( vector (( LC_CLSpace V),L2))) = (L1 + L2)

    proof

      set v2 = ( vector (( LC_CLSpace V),L2));

      

       A1: L1 = ( @ ( @ L1)) & L2 = ( @ ( @ L2));

      L2 in the carrier of ( LC_CLSpace V) by Def12;

      then

       A2: L2 in ( LC_CLSpace V);

      L1 in the carrier of ( LC_CLSpace V) by Def12;

      then L1 in ( LC_CLSpace V);

      

      hence (( vector (( LC_CLSpace V),L1)) + ( vector (( LC_CLSpace V),L2))) = (( C_LCAdd V) . [L1, v2]) by RLVECT_2:def 1

      .= (( C_LCAdd V) . (( @ L1),( @ L2))) by A2, RLVECT_2:def 1

      .= (L1 + L2) by A1, Def15;

    end;

    theorem :: CONVEX4:39

    

     Th39: (a * ( vector (( LC_CLSpace V),L))) = (a * L)

    proof

      L in the carrier of ( LC_CLSpace V) by Def12;

      then L in ( LC_CLSpace V);

      then

       A1: (( C_LCMult V) . [a, ( vector (( LC_CLSpace V),L))]) = (( C_LCMult V) . [a, ( @ L)]) by RLVECT_2:def 1;

      ( @ ( @ L)) = L;

      hence thesis by A1, Def16;

    end;

    theorem :: CONVEX4:40

    

     Th40: ( - ( vector (( LC_CLSpace V),L))) = ( - L)

    proof

      

      thus ( - ( vector (( LC_CLSpace V),L))) = (( - 1r ) * ( vector (( LC_CLSpace V),L))) by CLVECT_1: 3

      .= ( - L) by Th39;

    end;

    theorem :: CONVEX4:41

    (( vector (( LC_CLSpace V),L1)) - ( vector (( LC_CLSpace V),L2))) = (L1 - L2)

    proof

      ( - L2) in ( C_LinComb V) by Def12;

      then

       A1: ( - L2) in ( LC_CLSpace V);

      ( - ( vector (( LC_CLSpace V),L2))) = ( - L2) by Th40

      .= ( vector (( LC_CLSpace V),( - L2))) by A1, RLVECT_2:def 1;

      hence thesis by Th38;

    end;

    definition

      let V;

      let A;

      :: CONVEX4:def18

      func LC_CLSpace A -> strict Subspace of ( LC_CLSpace V) means the carrier of it = the set of all l;

      existence

      proof

        set X = the set of all l;

        X c= the carrier of ( LC_CLSpace V)

        proof

          let x be object;

          assume x in X;

          then ex l st x = l;

          hence thesis by Def12;

        end;

        then

        reconsider X as Subset of ( LC_CLSpace V);

        

         A1: for v,u be VECTOR of ( LC_CLSpace V) st v in X & u in X holds (v + u) in X

        proof

          let v,u be VECTOR of ( LC_CLSpace V);

          assume that

           A2: v in X and

           A3: u in X;

          consider l1 such that

           A4: v = l1 by A2;

          consider l2 such that

           A5: u = l2 by A3;

          

           A6: u = ( vector (( LC_CLSpace V),l2)) by A5, RLVECT_2: 1;

          v = ( vector (( LC_CLSpace V),l1)) by A4, RLVECT_2: 1;

          then (v + u) = (l1 + l2) by A6, Th38;

          hence thesis;

        end;

        ( ZeroCLC V) is C_Linear_Combination of A by Th4;

        then

         A7: ( ZeroCLC V) in X;

        for a be Complex, v be VECTOR of ( LC_CLSpace V) st v in X holds (a * v) in X

        proof

          let a be Complex;

          let v be VECTOR of ( LC_CLSpace V);

          assume v in X;

          then

          consider l such that

           A8: v = l;

          (a * v) = (a * ( vector (( LC_CLSpace V),l))) by A8, RLVECT_2: 1

          .= (a * l) by Th39;

          then (a * v) is C_Linear_Combination of A by Th26;

          hence thesis;

        end;

        then X is linearly-closed by A1;

        hence thesis by A7, CLVECT_1: 54;

      end;

      uniqueness by CLVECT_1: 49;

    end

    begin

    definition

      let V be ComplexLinearSpace, W be Subspace of V;

      :: CONVEX4:def19

      func Up W -> Subset of V equals the carrier of W;

      coherence by CLVECT_1:def 8;

    end

    registration

      let V be ComplexLinearSpace, W be Subspace of V;

      cluster ( Up W) -> non empty;

      coherence ;

    end

    definition

      let V be non empty CLSStruct, S be Subset of V;

      :: CONVEX4:def20

      attr S is Affine means for x,y be VECTOR of V, z be Complex st z is Real & x in S & y in S holds ((( 1r - z) * x) + (z * y)) in S;

    end

    definition

      let V be ComplexLinearSpace;

      :: CONVEX4:def21

      func (Omega). V -> strict Subspace of V equals the CLSStruct of V;

      coherence

      proof

        set W = the CLSStruct of V;

        

         A1: for v,w be VECTOR of W holds (v + w) = (w + v)

        proof

          let v,w be VECTOR of W;

          reconsider v9 = v, w9 = w as VECTOR of V;

          (v + w) = (v9 + w9);

          

          hence (v + w) = (w9 + v9)

          .= (w + v);

        end;

        

         A2: for u,v,w be VECTOR of W holds ((u + v) + w) = (u + (v + w))

        proof

          let u,v,w be VECTOR of W;

          reconsider u9 = u, v9 = v, w9 = w as VECTOR of V;

          ((u9 + v9) + w9) = (u9 + (v9 + w9)) by RLVECT_1:def 3;

          hence thesis;

        end;

        

         A3: for v be VECTOR of W holds v is right_complementable

        proof

          let v be VECTOR of W;

          reconsider v9 = v as VECTOR of V;

          v9 is right_complementable by ALGSTR_0:def 16;

          then

          consider w9 be VECTOR of V such that

           A4: (v9 + w9) = ( 0. V);

          reconsider w = w9 as VECTOR of W;

          take w;

          thus thesis by A4;

        end;

        

         A5: for v be VECTOR of W holds (v + ( 0. W)) = v

        proof

          let v be VECTOR of W;

          reconsider v9 = v as VECTOR of V;

          

          thus (v + ( 0. W)) = (v9 + ( 0. V))

          .= v;

        end;

        

         A6: for a, b holds for v be VECTOR of W holds ((a * b) * v) = (a * (b * v))

        proof

          let a, b;

          let v be VECTOR of W;

          reconsider v9 = v as VECTOR of V;

          ((a * b) * v9) = (a * (b * v9)) by CLVECT_1:def 4;

          hence thesis;

        end;

        

         A7: for a, b holds for v be VECTOR of W holds ((a + b) * v) = ((a * v) + (b * v))

        proof

          let a, b;

          let v be VECTOR of W;

          reconsider v9 = v as VECTOR of V;

          ((a + b) * v9) = ((a * v9) + (b * v9)) by CLVECT_1:def 3;

          hence thesis;

        end;

        

         A8: for a holds for v,w be VECTOR of W holds (a * (v + w)) = ((a * v) + (a * w))

        proof

          let a;

          let v,w be VECTOR of W;

          reconsider v9 = v, w9 = w as VECTOR of V;

          (a * (v9 + w9)) = ((a * v9) + (a * w9)) by CLVECT_1:def 2;

          hence thesis;

        end;

        for v be VECTOR of W holds ( 1r * v) = v

        proof

          let v be VECTOR of W;

          reconsider v9 = v as VECTOR of V;

          

          thus ( 1r * v) = ( 1r * v9)

          .= v by CLVECT_1:def 5;

        end;

        then

        reconsider W as ComplexLinearSpace by A1, A2, A5, A3, A8, A7, A6, ALGSTR_0:def 16, CLVECT_1:def 2, CLVECT_1:def 3, CLVECT_1:def 4, CLVECT_1:def 5, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4;

        

         A9: the Mult of W = (the Mult of V | [: COMPLEX , the carrier of W:]) by RELSET_1: 19;

        ( 0. W) = ( 0. V) & the addF of W = (the addF of V || the carrier of W) by RELSET_1: 19;

        hence thesis by A9, CLVECT_1:def 8;

      end;

    end

    registration

      let V be non empty CLSStruct;

      cluster ( [#] V) -> Affine;

      coherence ;

      cluster empty -> Affine for Subset of V;

      coherence ;

    end

    registration

      let V be non empty CLSStruct;

      cluster non empty Affine for Subset of V;

      existence

      proof

        take ( [#] V);

        thus thesis;

      end;

      cluster empty Affine for Subset of V;

      existence

      proof

        take ( {} V);

        thus thesis;

      end;

    end

    theorem :: CONVEX4:42

    

     Th42: for a be Real, z be Complex holds ( Re (a * z)) = (a * ( Re z))

    proof

      let a be Real;

      let z be Complex;

      ( Re (a * z)) = ((( Re a) * ( Re z)) - (( Im a) * ( Im z))) by COMPLEX1: 9

      .= ((( Re a) * ( Re z)) - ( 0 * ( Im z))) by COMPLEX1:def 2

      .= (a * ( Re z)) by COMPLEX1:def 1;

      hence thesis;

    end;

    theorem :: CONVEX4:43

    

     Th43: for a be Real, z be Complex holds ( Im (a * z)) = (a * ( Im z))

    proof

      let a be Real;

      let z be Complex;

      ( Im (a * z)) = ((( Re a) * ( Im z)) + (( Re z) * ( Im a))) by COMPLEX1: 9

      .= ((( Re a) * ( Im z)) + (( Re z) * 0 )) by COMPLEX1:def 2

      .= (a * ( Im z)) by COMPLEX1:def 1;

      hence thesis;

    end;

    theorem :: CONVEX4:44

    

     Th44: for a be Real, z be Complex st 0 <= a & a <= 1 holds |.(a * z).| = (a * |.z.|) & |.(( 1r - a) * z).| = (( 1r - a) * |.z.|)

    proof

      let a be Real;

      let z be Complex;

      assume that

       A1: 0 <= a and

       A2: a <= 1;

      

       A3: |.(( 1r - a) * z).| = ( |.( 1r - a).| * |.z.|) by COMPLEX1: 65

      .= (( 1r - a) * |.z.|) by A2, COMPLEX1: 43, XREAL_1: 48;

       |.(a * z).| = ( |.a.| * |.z.|) by COMPLEX1: 65

      .= (a * |.z.|) by A1, COMPLEX1: 43;

      hence thesis by A3;

    end;

    begin

    definition

      let V be non empty CLSStruct;

      let M be Subset of V;

      let r be Complex;

      :: CONVEX4:def22

      func r * M -> Subset of V equals { (r * v) where v be Element of V : v in M };

      coherence

      proof

        deffunc F( Element of V) = (r * $1);

        defpred P[ set] means $1 in M;

        { F(v) where v be Element of V : P[v] } is Subset of V from DOMAIN_1:sch 8;

        hence thesis;

      end;

    end

    definition

      let V be non empty CLSStruct;

      let M be Subset of V;

      :: CONVEX4:def23

      attr M is convex means for u,v be VECTOR of V, z be Complex st (ex r be Real st z = r & 0 < r & r < 1) & u in M & v in M holds ((z * u) + (( 1r - z) * v)) in M;

    end

    theorem :: CONVEX4:45

    for V be vector-distributive scalar-distributive scalar-associative scalar-unital non empty CLSStruct, M be Subset of V, z be Complex st M is convex holds (z * M) is convex

    proof

      let V be vector-distributive scalar-distributive scalar-associative scalar-unital non empty CLSStruct;

      let M be Subset of V;

      let z be Complex;

      assume

       A1: M is convex;

      for u,v be VECTOR of V, s be Complex st (ex p be Real st s = p & 0 < p & p < 1) & u in (z * M) & v in (z * M) holds ((s * u) + (( 1r - s) * v)) in (z * M)

      proof

        let u,v be VECTOR of V;

        let s be Complex;

        assume that

         A2: ex p be Real st s = p & 0 < p & p < 1 and

         A3: u in (z * M) and

         A4: v in (z * M);

        consider v9 be Element of V such that

         A5: v = (z * v9) and

         A6: v9 in M by A4;

        consider u9 be Element of V such that

         A7: u = (z * u9) and

         A8: u9 in M by A3;

        

         A9: ((s * u) + (( 1r - s) * v)) = (((s * z) * u9) + (( 1r - s) * (z * v9))) by A7, A5, CLVECT_1:def 4

        .= (((z * s) * u9) + ((z * ( 1r - s)) * v9)) by CLVECT_1:def 4

        .= ((z * (s * u9)) + ((z * ( 1r - s)) * v9)) by CLVECT_1:def 4

        .= ((z * (s * u9)) + (z * (( 1r - s) * v9))) by CLVECT_1:def 4

        .= (z * ((s * u9) + (( 1r - s) * v9))) by CLVECT_1:def 2;

        ((s * u9) + (( 1r - s) * v9)) in M by A1, A2, A8, A6;

        hence thesis by A9;

      end;

      hence thesis;

    end;

    theorem :: CONVEX4:46

    for V be Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital non empty CLSStruct, M,N be Subset of V st M is convex & N is convex holds (M + N) is convex

    proof

      let V be Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital non empty CLSStruct;

      let M,N be Subset of V;

      assume

       A1: M is convex & N is convex;

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

      proof

        let u,v be VECTOR of V;

        let z be Complex;

        assume that

         A2: ex r be Real st z = r & 0 < r & r < 1 and

         A3: u in (M + N) and

         A4: v in (M + N);

        consider x2,y2 be Element of V such that

         A5: v = (x2 + y2) and

         A6: x2 in M & y2 in N by A4;

        consider x1,y1 be Element of V such that

         A7: u = (x1 + y1) and

         A8: x1 in M & y1 in N by A3;

        

         A9: ((z * u) + (( 1r - z) * v)) = (((z * x1) + (z * y1)) + (( 1r - z) * (x2 + y2))) by A7, A5, CLVECT_1:def 2

        .= (((z * x1) + (z * y1)) + ((( 1r - z) * x2) + (( 1r - z) * y2))) by CLVECT_1:def 2

        .= ((((z * x1) + (z * y1)) + (( 1r - z) * x2)) + (( 1r - z) * y2)) by RLVECT_1:def 3

        .= ((((z * x1) + (( 1r - z) * x2)) + (z * y1)) + (( 1r - z) * y2)) by RLVECT_1:def 3

        .= (((z * x1) + (( 1r - z) * x2)) + ((z * y1) + (( 1r - z) * y2))) by RLVECT_1:def 3;

        ((z * x1) + (( 1r - z) * x2)) in M & ((z * y1) + (( 1r - z) * y2)) in N by A1, A2, A8, A6;

        hence thesis by A9;

      end;

      hence thesis;

    end;

    theorem :: CONVEX4:47

    for V be ComplexLinearSpace, M,N be Subset of V st M is convex & N is convex holds (M - N) is convex

    proof

      let V be ComplexLinearSpace;

      let M,N be Subset of V;

      assume

       A1: M is convex & N is convex;

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

      proof

        let u,v be VECTOR of V;

        let z be Complex;

        assume that

         A2: ex r be Real st z = r & 0 < r & r < 1 and

         A3: u in (M - N) and

         A4: v in (M - N);

        consider x2,y2 be Element of V such that

         A5: v = (x2 - y2) and

         A6: x2 in M & y2 in N by A4;

        consider x1,y1 be Element of V such that

         A7: u = (x1 - y1) and

         A8: x1 in M & y1 in N by A3;

        

         A9: ((z * u) + (( 1r - z) * v)) = (((z * x1) - (z * y1)) + (( 1r - z) * (x2 - y2))) by A7, A5, CLVECT_1: 9

        .= (((z * x1) - (z * y1)) + ((( 1r - z) * x2) - (( 1r - z) * y2))) by CLVECT_1: 9

        .= ((((z * x1) - (z * y1)) + (( 1r - z) * x2)) - (( 1r - z) * y2)) by RLVECT_1:def 3

        .= (((z * x1) - ((z * y1) - (( 1r - z) * x2))) - (( 1r - z) * y2)) by RLVECT_1: 29

        .= (((z * x1) + ((( 1r - z) * x2) + ( - (z * y1)))) - (( 1r - z) * y2)) by RLVECT_1: 33

        .= ((((z * x1) + (( 1r - z) * x2)) + ( - (z * y1))) - (( 1r - z) * y2)) by RLVECT_1:def 3

        .= (((z * x1) + (( 1r - z) * x2)) + (( - (z * y1)) - (( 1r - z) * y2))) by RLVECT_1:def 3

        .= (((z * x1) + (( 1r - z) * x2)) - ((z * y1) + (( 1r - z) * y2))) by RLVECT_1: 30;

        ((z * x1) + (( 1r - z) * x2)) in M & ((z * y1) + (( 1r - z) * y2)) in N by A1, A2, A8, A6;

        hence thesis by A9;

      end;

      hence thesis;

    end;

    theorem :: CONVEX4:48

    

     Th48: for V be non empty CLSStruct, M be Subset of V holds M is convex iff for z be Complex st (ex r be Real st z = r & 0 < r & r < 1) holds ((z * M) + (( 1r - z) * M)) c= M

    proof

      let V be non empty CLSStruct;

      let M be Subset of V;

      

       A1: M is convex implies for z be Complex st (ex r be Real st z = r & 0 < r & r < 1) holds ((z * M) + (( 1r - z) * M)) c= M

      proof

        assume

         A2: M is convex;

        let z be Complex;

        assume

         A3: ex r be Real st z = r & 0 < r & r < 1;

        for x be Element of V st x in ((z * M) + (( 1r - z) * M)) holds x in M

        proof

          let x be Element of V;

          assume x in ((z * M) + (( 1r - z) * M));

          then

          consider u,v be Element of V such that

           A4: x = (u + v) and

           A5: u in (z * M) & v in (( 1r - z) * M);

          (ex w1 be Element of V st u = (z * w1) & w1 in M) & ex w2 be Element of V st v = (( 1r - z) * w2) & w2 in M by A5;

          hence thesis by A2, A3, A4;

        end;

        hence thesis;

      end;

      (for z be Complex st (ex r be Real st z = r & 0 < r & r < 1) holds ((z * M) + (( 1r - z) * M)) c= M) implies M is convex

      proof

        assume

         A6: for z be Complex st (ex r be Real st z = r & 0 < r & r < 1) holds ((z * M) + (( 1r - z) * M)) c= M;

        let u,v be VECTOR of V;

        let z be Complex;

        assume ex r be Real st z = r & 0 < r & r < 1;

        then

         A7: ((z * M) + (( 1r - z) * M)) c= M by A6;

        assume u in M & v in M;

        then (z * u) in (z * M) & (( 1r - z) * v) in (( 1r - z) * M);

        then ((z * u) + (( 1r - z) * v)) in ((z * M) + (( 1r - z) * M));

        hence thesis by A7;

      end;

      hence thesis by A1;

    end;

    theorem :: CONVEX4:49

    for V be Abelian non empty CLSStruct, M be Subset of V st M is convex holds for z be Complex st (ex r be Real st z = r & 0 < r & r < 1) holds ((( 1r - z) * M) + (z * M)) c= M

    proof

      let V be Abelian non empty CLSStruct;

      let M be Subset of V;

      assume

       A1: M is convex;

      let z be Complex;

      assume

       A2: ex r be Real st z = r & 0 < r & r < 1;

      for x be Element of V st x in ((( 1r - z) * M) + (z * M)) holds x in M

      proof

        let x be Element of V;

        assume x in ((( 1r - z) * M) + (z * M));

        then

        consider u,v be Element of V such that

         A3: x = (u + v) and

         A4: u in (( 1r - z) * M) & v in (z * M);

        (ex w1 be Element of V st u = (( 1r - z) * w1) & w1 in M) & ex w2 be Element of V st v = (z * w2) & w2 in M by A4;

        hence thesis by A1, A2, A3;

      end;

      hence thesis;

    end;

    theorem :: CONVEX4:50

    for V be Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital non empty CLSStruct, M,N be Subset of V st M is convex & N is convex holds for z be Complex holds ((z * M) + (( 1r - z) * N)) is convex

    proof

      let V be Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital non empty CLSStruct;

      let M,N be Subset of V;

      assume that

       A1: M is convex and

       A2: N is convex;

      let z be Complex;

      let u,v be VECTOR of V;

      let s be Complex;

      assume that

       A3: ex p be Real st s = p & 0 < p & p < 1 and

       A4: u in ((z * M) + (( 1r - z) * N)) and

       A5: v in ((z * M) + (( 1r - z) * N));

      consider x2,y2 be VECTOR of V such that

       A6: v = (x2 + y2) and

       A7: x2 in (z * M) and

       A8: y2 in (( 1r - z) * N) by A5;

      consider x1,y1 be VECTOR of V such that

       A9: u = (x1 + y1) and

       A10: x1 in (z * M) and

       A11: y1 in (( 1r - z) * N) by A4;

      consider mx2 be VECTOR of V such that

       A12: x2 = (z * mx2) and

       A13: mx2 in M by A7;

      consider mx1 be VECTOR of V such that

       A14: x1 = (z * mx1) and

       A15: mx1 in M by A10;

      

       A16: ((s * x1) + (( 1r - s) * x2)) = (((s * z) * mx1) + (( 1r - s) * (z * mx2))) by A14, A12, CLVECT_1:def 4

      .= (((s * z) * mx1) + ((( 1r - s) * z) * mx2)) by CLVECT_1:def 4

      .= ((z * (s * mx1)) + ((( 1r - s) * z) * mx2)) by CLVECT_1:def 4

      .= ((z * (s * mx1)) + (z * (( 1r - s) * mx2))) by CLVECT_1:def 4

      .= (z * ((s * mx1) + (( 1r - s) * mx2))) by CLVECT_1:def 2;

      consider ny2 be VECTOR of V such that

       A17: y2 = (( 1r - z) * ny2) and

       A18: ny2 in N by A8;

      consider ny1 be VECTOR of V such that

       A19: y1 = (( 1r - z) * ny1) and

       A20: ny1 in N by A11;

      

       A21: ((s * y1) + (( 1r - s) * y2)) = (((s * ( 1r - z)) * ny1) + (( 1r - s) * (( 1r - z) * ny2))) by A19, A17, CLVECT_1:def 4

      .= (((s * ( 1r - z)) * ny1) + ((( 1r - s) * ( 1r - z)) * ny2)) by CLVECT_1:def 4

      .= ((( 1r - z) * (s * ny1)) + ((( 1r - s) * ( 1r - z)) * ny2)) by CLVECT_1:def 4

      .= ((( 1r - z) * (s * ny1)) + (( 1r - z) * (( 1r - s) * ny2))) by CLVECT_1:def 4

      .= (( 1r - z) * ((s * ny1) + (( 1r - s) * ny2))) by CLVECT_1:def 2;

      ((s * ny1) + (( 1r - s) * ny2)) in N by A2, A3, A20, A18;

      then

       A22: ((s * y1) + (( 1r - s) * y2)) in (( 1r - z) * N) by A21;

      ((s * mx1) + (( 1r - s) * mx2)) in M by A1, A3, A15, A13;

      then

       A23: ((s * x1) + (( 1r - s) * x2)) in (z * M) by A16;

      ((s * u) + (( 1r - s) * v)) = (((s * x1) + (s * y1)) + (( 1r - s) * (x2 + y2))) by A9, A6, CLVECT_1:def 2

      .= (((s * x1) + (s * y1)) + ((( 1r - s) * x2) + (( 1r - s) * y2))) by CLVECT_1:def 2

      .= ((((s * x1) + (s * y1)) + (( 1r - s) * x2)) + (( 1r - s) * y2)) by RLVECT_1:def 3

      .= ((((s * x1) + (( 1r - s) * x2)) + (s * y1)) + (( 1r - s) * y2)) by RLVECT_1:def 3

      .= (((s * x1) + (( 1r - s) * x2)) + ((s * y1) + (( 1r - s) * y2))) by RLVECT_1:def 3;

      hence thesis by A23, A22;

    end;

    theorem :: CONVEX4:51

    

     Th51: for V be vector-distributive scalar-distributive scalar-associative scalar-unital non empty CLSStruct, M be Subset of V holds ( 1r * M) = M

    proof

      let V be vector-distributive scalar-distributive scalar-associative scalar-unital non empty CLSStruct;

      let M be Subset of V;

      for v be Element of V st v in M holds v in ( 1r * M)

      proof

        let v be Element of V;

        

         A1: v = ( 1r * v) by CLVECT_1:def 5;

        assume v in M;

        hence thesis by A1;

      end;

      then

       A2: M c= ( 1r * M);

      for v be Element of V st v in ( 1r * M) holds v in M

      proof

        let v be Element of V;

        assume v in ( 1r * M);

        then ex x be Element of V st v = ( 1r * x) & x in M;

        hence thesis by CLVECT_1:def 5;

      end;

      then ( 1r * M) c= M;

      hence thesis by A2, XBOOLE_0:def 10;

    end;

    theorem :: CONVEX4:52

    

     Th52: for V be ComplexLinearSpace, M be non empty Subset of V holds ( 0c * M) = {( 0. V)}

    proof

      let V be ComplexLinearSpace;

      let M be non empty Subset of V;

      for v be Element of V st v in {( 0. V)} holds v in ( 0c * M)

      proof

        let v be Element of V;

        consider x be object such that

         A1: x in M by XBOOLE_0:def 1;

        reconsider x as Element of V by A1;

        assume v in {( 0. V)};

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

        then v = ( 0c * x) by CLVECT_1: 1;

        hence thesis by A1;

      end;

      then

       A2: {( 0. V)} c= ( 0c * M);

      for v be Element of V st v in ( 0c * M) holds v in {( 0. V)}

      proof

        let v be Element of V;

        assume v in ( 0c * M);

        then ex x be Element of V st v = ( 0c * x) & x in M;

        then v = ( 0. V) by CLVECT_1: 1;

        hence thesis by TARSKI:def 1;

      end;

      then ( 0c * M) c= {( 0. V)};

      hence thesis by A2, XBOOLE_0:def 10;

    end;

    ::$Canceled

    theorem :: CONVEX4:54

    

     Th53: for V be vector-distributive scalar-distributive scalar-associative scalar-unital non empty CLSStruct, M be Subset of V, z1,z2 be Complex holds (z1 * (z2 * M)) = ((z1 * z2) * M)

    proof

      let V be vector-distributive scalar-distributive scalar-associative scalar-unital non empty CLSStruct;

      let M be Subset of V;

      let z1,z2 be Complex;

      for x be VECTOR of V st x in (z1 * (z2 * M)) holds x in ((z1 * z2) * M)

      proof

        let x be VECTOR of V;

        assume x in (z1 * (z2 * M));

        then

        consider w1 be VECTOR of V such that

         A1: x = (z1 * w1) and

         A2: w1 in (z2 * M);

        consider w2 be VECTOR of V such that

         A3: w1 = (z2 * w2) and

         A4: w2 in M by A2;

        x = ((z1 * z2) * w2) by A1, A3, CLVECT_1:def 4;

        hence thesis by A4;

      end;

      then

       A5: (z1 * (z2 * M)) c= ((z1 * z2) * M);

      for x be VECTOR of V st x in ((z1 * z2) * M) holds x in (z1 * (z2 * M))

      proof

        let x be VECTOR of V;

        assume x in ((z1 * z2) * M);

        then

        consider w1 be VECTOR of V such that

         A6: x = ((z1 * z2) * w1) & w1 in M;

        x = (z1 * (z2 * w1)) & (z2 * w1) in (z2 * M) by A6, CLVECT_1:def 4;

        hence thesis;

      end;

      then ((z1 * z2) * M) c= (z1 * (z2 * M));

      hence thesis by A5, XBOOLE_0:def 10;

    end;

    theorem :: CONVEX4:55

    

     Th54: for V be vector-distributive scalar-distributive scalar-associative scalar-unital non empty CLSStruct, M1,M2 be Subset of V, z be Complex holds (z * (M1 + M2)) = ((z * M1) + (z * M2))

    proof

      let V be vector-distributive scalar-distributive scalar-associative scalar-unital non empty CLSStruct;

      let M1,M2 be Subset of V;

      let z be Complex;

      for x be VECTOR of V st x in ((z * M1) + (z * M2)) holds x in (z * (M1 + M2))

      proof

        let x be VECTOR of V;

        assume x in ((z * M1) + (z * M2));

        then

        consider w1,w2 be VECTOR of V such that

         A1: x = (w1 + w2) and

         A2: w1 in (z * M1) and

         A3: w2 in (z * M2);

        consider v2 be VECTOR of V such that

         A4: w2 = (z * v2) and

         A5: v2 in M2 by A3;

        consider v1 be VECTOR of V such that

         A6: w1 = (z * v1) and

         A7: v1 in M1 by A2;

        

         A8: (v1 + v2) in (M1 + M2) by A7, A5;

        x = (z * (v1 + v2)) by A1, A6, A4, CLVECT_1:def 2;

        hence thesis by A8;

      end;

      then

       A9: ((z * M1) + (z * M2)) c= (z * (M1 + M2));

      for x be VECTOR of V st x in (z * (M1 + M2)) holds x in ((z * M1) + (z * M2))

      proof

        let x be VECTOR of V;

        assume x in (z * (M1 + M2));

        then

        consider w9 be VECTOR of V such that

         A10: x = (z * w9) and

         A11: w9 in (M1 + M2);

        consider w1,w2 be VECTOR of V such that

         A12: w9 = (w1 + w2) and

         A13: w1 in M1 & w2 in M2 by A11;

        

         A14: (z * w1) in (z * M1) & (z * w2) in (z * M2) by A13;

        x = ((z * w1) + (z * w2)) by A10, A12, CLVECT_1:def 2;

        hence thesis by A14;

      end;

      then (z * (M1 + M2)) c= ((z * M1) + (z * M2));

      hence thesis by A9, XBOOLE_0:def 10;

    end;

    theorem :: CONVEX4:56

    for V be ComplexLinearSpace, M be Subset of V, v be VECTOR of V holds M is convex iff (v + M) is convex

    proof

      let V be ComplexLinearSpace;

      let M be Subset of V;

      let v be VECTOR of V;

      

       A1: (v + M) is convex implies M is convex

      proof

        assume

         A2: (v + M) is convex;

        let w1,w2 be VECTOR of V;

        let z be Complex;

        assume that

         A3: ex r be Real st z = r & 0 < r & r < 1 and

         A4: w1 in M & w2 in M;

        set x1 = (v + w1), x2 = (v + w2);

        x1 in (v + M) & x2 in { (v + w) where w be VECTOR of V : w in M } by A4;

        then

         A5: ((z * x1) + (( 1r - z) * x2)) in (v + M) by A2, A3;

        ((z * x1) + (( 1r - z) * x2)) = (((z * v) + (z * w1)) + (( 1r - z) * (v + w2))) by CLVECT_1:def 2

        .= (((z * v) + (z * w1)) + ((( 1r - z) * v) + (( 1r - z) * w2))) by CLVECT_1:def 2

        .= ((((z * v) + (z * w1)) + (( 1r - z) * v)) + (( 1r - z) * w2)) by RLVECT_1:def 3

        .= ((((z * v) + (( 1r - z) * v)) + (z * w1)) + (( 1r - z) * w2)) by RLVECT_1:def 3

        .= ((((z + ( 1r - z)) * v) + (z * w1)) + (( 1r - z) * w2)) by CLVECT_1:def 3

        .= ((v + (z * w1)) + (( 1r - z) * w2)) by CLVECT_1:def 5

        .= (v + ((z * w1) + (( 1r - z) * w2))) by RLVECT_1:def 3;

        then ex w be VECTOR of V st (v + ((z * w1) + (( 1r - z) * w2))) = (v + w) & w in M by A5;

        hence thesis by RLVECT_1: 8;

      end;

      M is convex implies (v + M) is convex

      proof

        assume

         A6: M is convex;

        let w1,w2 be VECTOR of V;

        let z be Complex;

        assume that

         A7: ex r be Real st z = r & 0 < r & r < 1 and

         A8: w1 in (v + M) and

         A9: w2 in (v + M);

        consider x2 be VECTOR of V such that

         A10: w2 = (v + x2) and

         A11: x2 in M by A9;

        consider x1 be VECTOR of V such that

         A12: w1 = (v + x1) and

         A13: x1 in M by A8;

        

         A14: ((z * w1) + (( 1r - z) * w2)) = (((z * v) + (z * x1)) + (( 1r - z) * (v + x2))) by A12, A10, CLVECT_1:def 2

        .= (((z * v) + (z * x1)) + ((( 1r - z) * v) + (( 1r - z) * x2))) by CLVECT_1:def 2

        .= ((((z * v) + (z * x1)) + (( 1r - z) * v)) + (( 1r - z) * x2)) by RLVECT_1:def 3

        .= ((((z * v) + (( 1r - z) * v)) + (z * x1)) + (( 1r - z) * x2)) by RLVECT_1:def 3

        .= ((((z + ( 1r - z)) * v) + (z * x1)) + (( 1r - z) * x2)) by CLVECT_1:def 3

        .= ((v + (z * x1)) + (( 1r - z) * x2)) by CLVECT_1:def 5

        .= (v + ((z * x1) + (( 1r - z) * x2))) by RLVECT_1:def 3;

        ((z * x1) + (( 1r - z) * x2)) in M by A6, A7, A13, A11;

        hence thesis by A14;

      end;

      hence thesis by A1;

    end;

    theorem :: CONVEX4:57

    for V be ComplexLinearSpace holds ( Up ( (0). V)) is convex

    proof

      let V be ComplexLinearSpace;

      let u,v be VECTOR of V;

      let z be Complex;

      assume that ex r be Real st z = r & 0 < r & r < 1 and

       A1: u in ( Up ( (0). V)) and

       A2: v in ( Up ( (0). V));

      v in {( 0. V)} by A2, CLVECT_1:def 9;

      then

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

      u in {( 0. V)} by A1, CLVECT_1:def 9;

      then u = ( 0. V) by TARSKI:def 1;

      

      then ((z * u) + (( 1r - z) * v)) = (( 0. V) + (( 1r - z) * ( 0. V))) by A3, CLVECT_1: 1

      .= (( 0. V) + ( 0. V)) by CLVECT_1: 1

      .= ( 0. V);

      then ((z * u) + (( 1r - z) * v)) in {( 0. V)} by TARSKI:def 1;

      hence thesis by CLVECT_1:def 9;

    end;

    theorem :: CONVEX4:58

    for V be ComplexLinearSpace holds ( Up ( (Omega). V)) is convex;

    theorem :: CONVEX4:59

    for V be non empty CLSStruct, M be Subset of V st M = {} holds M is convex;

    theorem :: CONVEX4:60

    

     Th59: for V be Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital non empty CLSStruct, M1,M2 be Subset of V, z1,z2 be Complex st M1 is convex & M2 is convex holds ((z1 * M1) + (z2 * M2)) is convex

    proof

      let V be Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital non empty CLSStruct;

      let M1,M2 be Subset of V;

      let z1,z2 be Complex;

      assume that

       A1: M1 is convex and

       A2: M2 is convex;

      let u,v be VECTOR of V;

      let s be Complex;

      assume that

       A3: ex p be Real st s = p & 0 < p & p < 1 and

       A4: u in ((z1 * M1) + (z2 * M2)) and

       A5: v in ((z1 * M1) + (z2 * M2));

      consider v1,v2 be VECTOR of V such that

       A6: v = (v1 + v2) and

       A7: v1 in (z1 * M1) and

       A8: v2 in (z2 * M2) by A5;

      consider u1,u2 be VECTOR of V such that

       A9: u = (u1 + u2) and

       A10: u1 in (z1 * M1) and

       A11: u2 in (z2 * M2) by A4;

      consider y1 be VECTOR of V such that

       A12: v1 = (z1 * y1) and

       A13: y1 in M1 by A7;

      consider x1 be VECTOR of V such that

       A14: u1 = (z1 * x1) and

       A15: x1 in M1 by A10;

      

       A16: ((s * u1) + (( 1r - s) * v1)) = (((z1 * s) * x1) + (( 1r - s) * (z1 * y1))) by A14, A12, CLVECT_1:def 4

      .= (((z1 * s) * x1) + ((z1 * ( 1r - s)) * y1)) by CLVECT_1:def 4

      .= ((z1 * (s * x1)) + ((z1 * ( 1r - s)) * y1)) by CLVECT_1:def 4

      .= ((z1 * (s * x1)) + (z1 * (( 1r - s) * y1))) by CLVECT_1:def 4

      .= (z1 * ((s * x1) + (( 1r - s) * y1))) by CLVECT_1:def 2;

      consider y2 be VECTOR of V such that

       A17: v2 = (z2 * y2) and

       A18: y2 in M2 by A8;

      consider x2 be VECTOR of V such that

       A19: u2 = (z2 * x2) and

       A20: x2 in M2 by A11;

      

       A21: ((s * u2) + (( 1r - s) * v2)) = (((z2 * s) * x2) + (( 1r - s) * (z2 * y2))) by A19, A17, CLVECT_1:def 4

      .= (((z2 * s) * x2) + ((z2 * ( 1r - s)) * y2)) by CLVECT_1:def 4

      .= ((z2 * (s * x2)) + ((z2 * ( 1r - s)) * y2)) by CLVECT_1:def 4

      .= ((z2 * (s * x2)) + (z2 * (( 1r - s) * y2))) by CLVECT_1:def 4

      .= (z2 * ((s * x2) + (( 1r - s) * y2))) by CLVECT_1:def 2;

      ((s * x2) + (( 1r - s) * y2)) in M2 by A2, A3, A20, A18;

      then

       A22: ((s * u2) + (( 1r - s) * v2)) in (z2 * M2) by A21;

      ((s * x1) + (( 1r - s) * y1)) in M1 by A1, A3, A15, A13;

      then

       A23: ((s * u1) + (( 1r - s) * v1)) in (z1 * M1) by A16;

      ((s * (u1 + u2)) + (( 1r - s) * (v1 + v2))) = (((s * u1) + (s * u2)) + (( 1r - s) * (v1 + v2))) by CLVECT_1:def 2

      .= (((s * u1) + (s * u2)) + ((( 1r - s) * v1) + (( 1r - s) * v2))) by CLVECT_1:def 2

      .= ((((s * u1) + (s * u2)) + (( 1r - s) * v1)) + (( 1r - s) * v2)) by RLVECT_1:def 3

      .= ((((s * u1) + (( 1r - s) * v1)) + (s * u2)) + (( 1r - s) * v2)) by RLVECT_1:def 3

      .= (((s * u1) + (( 1r - s) * v1)) + ((s * u2) + (( 1r - s) * v2))) by RLVECT_1:def 3;

      hence thesis by A9, A6, A23, A22;

    end;

    theorem :: CONVEX4:61

    

     Th60: for V be vector-distributive scalar-distributive scalar-associative scalar-unital non empty CLSStruct, M be Subset of V, z1,z2 be Complex holds ((z1 + z2) * M) c= ((z1 * M) + (z2 * M))

    proof

      let V be vector-distributive scalar-distributive scalar-associative scalar-unital non empty CLSStruct;

      let M be Subset of V;

      let z1,z2 be Complex;

      for x be VECTOR of V st x in ((z1 + z2) * M) holds x in ((z1 * M) + (z2 * M))

      proof

        let x be VECTOR of V;

        assume x in ((z1 + z2) * M);

        then

        consider w be VECTOR of V such that

         A1: x = ((z1 + z2) * w) and

         A2: w in M;

        

         A3: (z2 * w) in (z2 * M) by A2;

        x = ((z1 * w) + (z2 * w)) & (z1 * w) in (z1 * M) by A1, A2, CLVECT_1:def 3;

        hence thesis by A3;

      end;

      hence thesis;

    end;

    theorem :: CONVEX4:62

    

     Th61: for V be non empty CLSStruct, M,N be Subset of V, z be Complex st M c= N holds (z * M) c= (z * N)

    proof

      let V be non empty CLSStruct;

      let M,N be Subset of V;

      let z be Complex;

      assume

       A1: M c= N;

      now

        let x be VECTOR of V;

        assume x in (z * M);

        then ex w be VECTOR of V st x = (z * w) & w in M;

        hence x in (z * N) by A1;

      end;

      hence thesis;

    end;

    theorem :: CONVEX4:63

    

     Th62: for V be non empty CLSStruct, M be empty Subset of V, z be Complex holds (z * M) = {}

    proof

      let V be non empty CLSStruct;

      let M be empty Subset of V;

      let z be Complex;

      now

        let x be VECTOR of V;

        assume x in (z * M);

        then ex v be VECTOR of V st x = (z * v) & v in {} ;

        hence x in {} ;

      end;

      then (z * M) c= {} ;

      hence thesis;

    end;

    

     Lm2: for V be ComplexLinearSpace, M be Subset of V, z1,z2 be Complex st (ex r1,r2 be Real st z1 = r1 & z2 = r2 & r1 >= 0 & r2 >= 0 ) & M is convex holds ((z1 * M) + (z2 * M)) c= ((z1 + z2) * M)

    proof

      let V be ComplexLinearSpace;

      let M be Subset of V;

      let z1,z2 be Complex;

      assume that

       A1: ex r1,r2 be Real st z1 = r1 & z2 = r2 & r1 >= 0 & r2 >= 0 and

       A2: M is convex;

      consider r1,r2 be Real such that

       A3: z1 = r1 and

       A4: z2 = r2 and

       A5: r1 >= 0 and

       A6: r2 >= 0 by A1;

      per cases ;

        suppose M is empty;

        then (z1 * M) = {} & ((z1 + z2) * M) = {} by Th62;

        hence thesis by CONVEX1: 40;

      end;

        suppose

         A7: M is non empty;

        per cases ;

          suppose

           A8: z1 = 0 ;

          then (z1 * M) = {( 0. V)} by A7, Th52;

          hence thesis by A8, CONVEX1: 35;

        end;

          suppose

           A9: z2 = 0 ;

          then (z2 * M) = {( 0. V)} by A7, Th52;

          hence thesis by A9, CONVEX1: 35;

        end;

          suppose

           A10: z1 <> 0 & z2 <> 0 ;

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

          then (r1 / (r1 + r2)) < 1 by A5, XREAL_1: 189;

          then (((z1 / (z1 + z2)) * M) + (( 1r - (z1 / (z1 + z2))) * M)) c= M by A2, A3, A4, A5, A6, A10, Th48;

          then

           A11: ((z1 + z2) * (((z1 / (z1 + z2)) * M) + (( 1r - (z1 / (z1 + z2))) * M))) c= ((z1 + z2) * M) by Th61;

          (1 - (r1 / (r1 + r2))) = (((r1 + r2) / (r1 + r2)) - (r1 / (r1 + r2))) by A3, A5, A6, A10, XCMPLX_1: 60;

          then (1 - (r1 / (r1 + r2))) = (((r1 + r2) - r1) / (r1 + r2));

          

          then

           A12: ((z1 + z2) * (( 1r - (z1 / (z1 + z2))) * M)) = (((z2 / (z1 + z2)) * (z1 + z2)) * M) by A3, A4, Th53

          .= (z2 * M) by A3, A4, A5, A6, A10, XCMPLX_1: 87;

          ((z1 + z2) * ((z1 / (z1 + z2)) * M)) = (((z1 / (z1 + z2)) * (z1 + z2)) * M) by Th53

          .= (z1 * M) by A3, A4, A5, A6, A10, XCMPLX_1: 87;

          hence thesis by A11, A12, Th54;

        end;

      end;

    end;

    ::$Canceled

    theorem :: CONVEX4:66

    for V be ComplexLinearSpace, M be Subset of V, z1,z2 be Complex st (ex r1,r2 be Real st z1 = r1 & z2 = r2 & r1 >= 0 & r2 >= 0 ) & M is convex holds ((z1 * M) + (z2 * M)) = ((z1 + z2) * M)

    proof

      let V be ComplexLinearSpace, M be Subset of V, z1,z2 be Complex;

      assume (ex r1,r2 be Real st z1 = r1 & z2 = r2 & r1 >= 0 & r2 >= 0 ) & M is convex;

      hence ((z1 * M) + (z2 * M)) c= ((z1 + z2) * M) by Lm2;

      thus thesis by Th60;

    end;

    theorem :: CONVEX4:67

    for V be Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital non empty CLSStruct, M1,M2,M3 be Subset of V, z1,z2,z3 be Complex st M1 is convex & M2 is convex & M3 is convex holds (((z1 * M1) + (z2 * M2)) + (z3 * M3)) is convex

    proof

      let V be Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital non empty CLSStruct;

      let M1,M2,M3 be Subset of V;

      let z1,z2,z3 be Complex;

      assume that

       A1: M1 is convex & M2 is convex and

       A2: M3 is convex;

      ((z1 * M1) + (z2 * M2)) is convex by A1, Th59;

      then (( 1r * ((z1 * M1) + (z2 * M2))) + (z3 * M3)) is convex by A2, Th59;

      hence thesis by Th51;

    end;

    theorem :: CONVEX4:68

    

     Th65: for V be non empty CLSStruct, F be Subset-Family of V st (for M be Subset of V st M in F holds M is convex) holds ( meet F) is convex

    proof

      let V be non empty CLSStruct;

      let F be Subset-Family of V;

      assume

       A1: for M be Subset of V st M in F holds M is convex;

      per cases ;

        suppose F = {} ;

        then ( meet F) = {} by SETFAM_1:def 1;

        hence thesis;

      end;

        suppose

         A2: F <> {} ;

        thus ( meet F) is convex

        proof

          let u,v be VECTOR of V;

          let z be Complex;

          assume that

           A3: ex r be Real st z = r & 0 < r & r < 1 and

           A4: u in ( meet F) and

           A5: v in ( meet F);

          for M be set st M in F holds ((z * u) + (( 1r - z) * v)) in M

          proof

            let M be set;

            assume

             A6: M in F;

            then

            reconsider M as Subset of V;

            

             A7: v in M by A5, A6, SETFAM_1:def 1;

            M is convex & u in M by A1, A4, A6, SETFAM_1:def 1;

            hence thesis by A3, A7;

          end;

          hence thesis by A2, SETFAM_1:def 1;

        end;

      end;

    end;

    theorem :: CONVEX4:69

    

     Th66: for V be non empty CLSStruct, M be Subset of V st M is Affine holds M is convex

    proof

      let V be non empty CLSStruct;

      let M be Subset of V;

      assume

       A1: M is Affine;

      let u,v be VECTOR of V;

      let z be Complex;

      assume that

       A2: ex r be Real st z = r & 0 < r & r < 1 and

       A3: u in M & v in M;

      set s = ( 1r - z);

      consider r be Real such that

       A4: z = r and 0 < r and r < 1 by A2;

      s = (1 - r) by A4;

      then ((( 1r - s) * u) + (s * v)) in M by A1, A3;

      hence thesis;

    end;

    registration

      let V be non empty CLSStruct;

      cluster non empty convex for Subset of V;

      existence

      proof

        set M = the non empty Affine Subset of V;

        M is convex by Th66;

        hence thesis;

      end;

    end

    registration

      let V be non empty CLSStruct;

      cluster empty convex for Subset of V;

      existence

      proof

        ( {} V) is convex;

        hence thesis;

      end;

    end

    theorem :: CONVEX4:70

    for V be ComplexUnitarySpace-like non empty CUNITSTR, M be Subset of V, v be VECTOR of V, r be Real st M = { u where u be VECTOR of V : ( Re (u .|. v)) >= r } holds M is convex

    proof

      let V be ComplexUnitarySpace-like non empty CUNITSTR;

      let M be Subset of V;

      let v be VECTOR of V;

      let r be Real;

      assume

       A1: M = { u where u be VECTOR of V : ( Re (u .|. v)) >= r };

      let x,y be VECTOR of V;

      let s be Complex;

      assume that

       A2: ex p be Real st s = p & 0 < p & p < 1 and

       A3: x in M and

       A4: y in M;

      

       A5: ex u2 be VECTOR of V st y = u2 & ( Re (u2 .|. v)) >= r by A1, A4;

      consider p be Real such that

       A6: s = p and

       A7: 0 < p and

       A8: p < 1 by A2;

      (1 - p) > 0 by A8, XREAL_1: 50;

      then

       A9: ((1 - p) * ( Re (y .|. v))) >= ((1 - p) * r) by A5, XREAL_1: 64;

      ex u1 be VECTOR of V st x = u1 & ( Re (u1 .|. v)) >= r by A1, A3;

      then (p * ( Re (x .|. v))) >= (p * r) by A7, XREAL_1: 64;

      then

       A10: ((p * ( Re (x .|. v))) + ((1 - p) * ( Re (y .|. v)))) >= ((p * r) + ((1 - p) * r)) by A9, XREAL_1: 7;

      ( Re (((s * x) + (( 1r - s) * y)) .|. v)) = ( Re (((s * x) .|. v) + ((( 1r - s) * y) .|. v))) by CSSPACE:def 13

      .= ( Re ((s * (x .|. v)) + ((( 1r - s) * y) .|. v))) by CSSPACE:def 13

      .= ( Re ((s * (x .|. v)) + (( 1r - s) * (y .|. v)))) by CSSPACE:def 13

      .= (( Re (s * (x .|. v))) + ( Re (( 1r - s) * (y .|. v)))) by COMPLEX1: 8

      .= ((p * ( Re (x .|. v))) + ( Re (( 1r - s) * (y .|. v)))) by A6, Th42

      .= ((p * ( Re (x .|. v))) + ((1 - p) * ( Re (y .|. v)))) by A6, Th42;

      hence thesis by A1, A10;

    end;

    theorem :: CONVEX4:71

    for V be ComplexUnitarySpace-like non empty CUNITSTR, M be Subset of V, v be VECTOR of V, r be Real st M = { u where u be VECTOR of V : ( Re (u .|. v)) > r } holds M is convex

    proof

      let V be ComplexUnitarySpace-like non empty CUNITSTR;

      let M be Subset of V;

      let v be VECTOR of V;

      let r be Real;

      assume

       A1: M = { u where u be VECTOR of V : ( Re (u .|. v)) > r };

      let x,y be VECTOR of V;

      let s be Complex;

      assume that

       A2: ex p be Real st s = p & 0 < p & p < 1 and

       A3: x in M and

       A4: y in M;

      

       A5: ex u2 be VECTOR of V st y = u2 & ( Re (u2 .|. v)) > r by A1, A4;

      consider p be Real such that

       A6: s = p and

       A7: 0 < p and

       A8: p < 1 by A2;

      (1 - p) > 0 by A8, XREAL_1: 50;

      then

       A9: ((1 - p) * ( Re (y .|. v))) > ((1 - p) * r) by A5, XREAL_1: 68;

      ex u1 be VECTOR of V st x = u1 & ( Re (u1 .|. v)) > r by A1, A3;

      then (p * ( Re (x .|. v))) > (p * r) by A7, XREAL_1: 68;

      then

       A10: ((p * ( Re (x .|. v))) + ((1 - p) * ( Re (y .|. v)))) > ((p * r) + ((1 - p) * r)) by A9, XREAL_1: 8;

      ( Re (((s * x) + (( 1r - s) * y)) .|. v)) = ( Re (((s * x) .|. v) + ((( 1r - s) * y) .|. v))) by CSSPACE:def 13

      .= ( Re ((s * (x .|. v)) + ((( 1r - s) * y) .|. v))) by CSSPACE:def 13

      .= ( Re ((s * (x .|. v)) + (( 1r - s) * (y .|. v)))) by CSSPACE:def 13

      .= (( Re (s * (x .|. v))) + ( Re (( 1r - s) * (y .|. v)))) by COMPLEX1: 8

      .= ((p * ( Re (x .|. v))) + ( Re (( 1r - s) * (y .|. v)))) by A6, Th42

      .= ((p * ( Re (x .|. v))) + ((1 - p) * ( Re (y .|. v)))) by A6, Th42;

      hence thesis by A1, A10;

    end;

    theorem :: CONVEX4:72

    for V be ComplexUnitarySpace-like non empty CUNITSTR, M be Subset of V, v be VECTOR of V, r be Real st M = { u where u be VECTOR of V : ( Re (u .|. v)) <= r } holds M is convex

    proof

      let V be ComplexUnitarySpace-like non empty CUNITSTR;

      let M be Subset of V;

      let v be VECTOR of V;

      let r be Real;

      assume

       A1: M = { u where u be VECTOR of V : ( Re (u .|. v)) <= r };

      let x,y be VECTOR of V;

      let s be Complex;

      assume that

       A2: ex p be Real st s = p & 0 < p & p < 1 and

       A3: x in M and

       A4: y in M;

      

       A5: ex u2 be VECTOR of V st y = u2 & ( Re (u2 .|. v)) <= r by A1, A4;

      consider p be Real such that

       A6: s = p and

       A7: 0 < p and

       A8: p < 1 by A2;

      (1 - p) > 0 by A8, XREAL_1: 50;

      then

       A9: ((1 - p) * ( Re (y .|. v))) <= ((1 - p) * r) by A5, XREAL_1: 64;

      ex u1 be VECTOR of V st x = u1 & ( Re (u1 .|. v)) <= r by A1, A3;

      then (p * ( Re (x .|. v))) <= (p * r) by A7, XREAL_1: 64;

      then

       A10: ((p * ( Re (x .|. v))) + ((1 - p) * ( Re (y .|. v)))) <= ((p * r) + ((1 - p) * r)) by A9, XREAL_1: 7;

      ( Re (((s * x) + (( 1r - s) * y)) .|. v)) = ( Re (((s * x) .|. v) + ((( 1r - s) * y) .|. v))) by CSSPACE:def 13

      .= ( Re ((s * (x .|. v)) + ((( 1r - s) * y) .|. v))) by CSSPACE:def 13

      .= ( Re ((s * (x .|. v)) + (( 1r - s) * (y .|. v)))) by CSSPACE:def 13

      .= (( Re (s * (x .|. v))) + ( Re (( 1r - s) * (y .|. v)))) by COMPLEX1: 8

      .= ((p * ( Re (x .|. v))) + ( Re (( 1r - s) * (y .|. v)))) by A6, Th42

      .= ((p * ( Re (x .|. v))) + ((1 - p) * ( Re (y .|. v)))) by A6, Th42;

      hence thesis by A1, A10;

    end;

    theorem :: CONVEX4:73

    for V be ComplexUnitarySpace-like non empty CUNITSTR, M be Subset of V, v be VECTOR of V, r be Real st M = { u where u be VECTOR of V : ( Re (u .|. v)) < r } holds M is convex

    proof

      let V be ComplexUnitarySpace-like non empty CUNITSTR;

      let M be Subset of V;

      let v be VECTOR of V;

      let r be Real;

      assume

       A1: M = { u where u be VECTOR of V : ( Re (u .|. v)) < r };

      let x,y be VECTOR of V;

      let s be Complex;

      assume that

       A2: ex p be Real st s = p & 0 < p & p < 1 and

       A3: x in M and

       A4: y in M;

      

       A5: ex u2 be VECTOR of V st y = u2 & ( Re (u2 .|. v)) < r by A1, A4;

      consider p be Real such that

       A6: s = p and

       A7: 0 < p and

       A8: p < 1 by A2;

      (1 - p) > 0 by A8, XREAL_1: 50;

      then

       A9: ((1 - p) * ( Re (y .|. v))) < ((1 - p) * r) by A5, XREAL_1: 68;

      ex u1 be VECTOR of V st x = u1 & ( Re (u1 .|. v)) < r by A1, A3;

      then (p * ( Re (x .|. v))) < (p * r) by A7, XREAL_1: 68;

      then

       A10: ((p * ( Re (x .|. v))) + ((1 - p) * ( Re (y .|. v)))) < ((p * r) + ((1 - p) * r)) by A9, XREAL_1: 8;

      ( Re (((s * x) + (( 1r - s) * y)) .|. v)) = ( Re (((s * x) .|. v) + ((( 1r - s) * y) .|. v))) by CSSPACE:def 13

      .= ( Re ((s * (x .|. v)) + ((( 1r - s) * y) .|. v))) by CSSPACE:def 13

      .= ( Re ((s * (x .|. v)) + (( 1r - s) * (y .|. v)))) by CSSPACE:def 13

      .= (( Re (s * (x .|. v))) + ( Re (( 1r - s) * (y .|. v)))) by COMPLEX1: 8

      .= ((p * ( Re (x .|. v))) + ( Re (( 1r - s) * (y .|. v)))) by A6, Th42

      .= ((p * ( Re (x .|. v))) + ((1 - p) * ( Re (y .|. v)))) by A6, Th42;

      hence thesis by A1, A10;

    end;

    theorem :: CONVEX4:74

    for V be ComplexUnitarySpace-like non empty CUNITSTR, M be Subset of V, v be VECTOR of V, r be Real st M = { u where u be VECTOR of V : ( Im (u .|. v)) >= r } holds M is convex

    proof

      let V be ComplexUnitarySpace-like non empty CUNITSTR;

      let M be Subset of V;

      let v be VECTOR of V;

      let r be Real;

      assume

       A1: M = { u where u be VECTOR of V : ( Im (u .|. v)) >= r };

      let x,y be VECTOR of V;

      let s be Complex;

      assume that

       A2: ex p be Real st s = p & 0 < p & p < 1 and

       A3: x in M and

       A4: y in M;

      

       A5: ex u2 be VECTOR of V st y = u2 & ( Im (u2 .|. v)) >= r by A1, A4;

      consider p be Real such that

       A6: s = p and

       A7: 0 < p and

       A8: p < 1 by A2;

      (1 - p) > 0 by A8, XREAL_1: 50;

      then

       A9: ((1 - p) * ( Im (y .|. v))) >= ((1 - p) * r) by A5, XREAL_1: 64;

      ex u1 be VECTOR of V st x = u1 & ( Im (u1 .|. v)) >= r by A1, A3;

      then (p * ( Im (x .|. v))) >= (p * r) by A7, XREAL_1: 64;

      then

       A10: ((p * ( Im (x .|. v))) + ((1 - p) * ( Im (y .|. v)))) >= ((p * r) + ((1 - p) * r)) by A9, XREAL_1: 7;

      ( Im (((s * x) + (( 1r - s) * y)) .|. v)) = ( Im (((s * x) .|. v) + ((( 1r - s) * y) .|. v))) by CSSPACE:def 13

      .= ( Im ((s * (x .|. v)) + ((( 1r - s) * y) .|. v))) by CSSPACE:def 13

      .= ( Im ((s * (x .|. v)) + (( 1r - s) * (y .|. v)))) by CSSPACE:def 13

      .= (( Im (s * (x .|. v))) + ( Im (( 1r - s) * (y .|. v)))) by COMPLEX1: 8

      .= ((p * ( Im (x .|. v))) + ( Im (( 1r - s) * (y .|. v)))) by A6, Th43

      .= ((p * ( Im (x .|. v))) + ((1 - p) * ( Im (y .|. v)))) by A6, Th43;

      hence thesis by A1, A10;

    end;

    theorem :: CONVEX4:75

    for V be ComplexUnitarySpace-like non empty CUNITSTR, M be Subset of V, v be VECTOR of V, r be Real st M = { u where u be VECTOR of V : ( Im (u .|. v)) > r } holds M is convex

    proof

      let V be ComplexUnitarySpace-like non empty CUNITSTR;

      let M be Subset of V;

      let v be VECTOR of V;

      let r be Real;

      assume

       A1: M = { u where u be VECTOR of V : ( Im (u .|. v)) > r };

      let x,y be VECTOR of V;

      let s be Complex;

      assume that

       A2: ex p be Real st s = p & 0 < p & p < 1 and

       A3: x in M and

       A4: y in M;

      

       A5: ex u2 be VECTOR of V st y = u2 & ( Im (u2 .|. v)) > r by A1, A4;

      consider p be Real such that

       A6: s = p and

       A7: 0 < p and

       A8: p < 1 by A2;

      (1 - p) > 0 by A8, XREAL_1: 50;

      then

       A9: ((1 - p) * ( Im (y .|. v))) > ((1 - p) * r) by A5, XREAL_1: 68;

      ex u1 be VECTOR of V st x = u1 & ( Im (u1 .|. v)) > r by A1, A3;

      then (p * ( Im (x .|. v))) > (p * r) by A7, XREAL_1: 68;

      then

       A10: ((p * ( Im (x .|. v))) + ((1 - p) * ( Im (y .|. v)))) > ((p * r) + ((1 - p) * r)) by A9, XREAL_1: 8;

      ( Im (((s * x) + (( 1r - s) * y)) .|. v)) = ( Im (((s * x) .|. v) + ((( 1r - s) * y) .|. v))) by CSSPACE:def 13

      .= ( Im ((s * (x .|. v)) + ((( 1r - s) * y) .|. v))) by CSSPACE:def 13

      .= ( Im ((s * (x .|. v)) + (( 1r - s) * (y .|. v)))) by CSSPACE:def 13

      .= (( Im (s * (x .|. v))) + ( Im (( 1r - s) * (y .|. v)))) by COMPLEX1: 8

      .= ((p * ( Im (x .|. v))) + ( Im (( 1r - s) * (y .|. v)))) by A6, Th43

      .= ((p * ( Im (x .|. v))) + ((1 - p) * ( Im (y .|. v)))) by A6, Th43;

      hence thesis by A1, A10;

    end;

    theorem :: CONVEX4:76

    for V be ComplexUnitarySpace-like non empty CUNITSTR, M be Subset of V, v be VECTOR of V, r be Real st M = { u where u be VECTOR of V : ( Im (u .|. v)) <= r } holds M is convex

    proof

      let V be ComplexUnitarySpace-like non empty CUNITSTR;

      let M be Subset of V;

      let v be VECTOR of V;

      let r be Real;

      assume

       A1: M = { u where u be VECTOR of V : ( Im (u .|. v)) <= r };

      let x,y be VECTOR of V;

      let s be Complex;

      assume that

       A2: ex p be Real st s = p & 0 < p & p < 1 and

       A3: x in M and

       A4: y in M;

      

       A5: ex u2 be VECTOR of V st y = u2 & ( Im (u2 .|. v)) <= r by A1, A4;

      consider p be Real such that

       A6: s = p and

       A7: 0 < p and

       A8: p < 1 by A2;

      (1 - p) > 0 by A8, XREAL_1: 50;

      then

       A9: ((1 - p) * ( Im (y .|. v))) <= ((1 - p) * r) by A5, XREAL_1: 64;

      ex u1 be VECTOR of V st x = u1 & ( Im (u1 .|. v)) <= r by A1, A3;

      then (p * ( Im (x .|. v))) <= (p * r) by A7, XREAL_1: 64;

      then

       A10: ((p * ( Im (x .|. v))) + ((1 - p) * ( Im (y .|. v)))) <= ((p * r) + ((1 - p) * r)) by A9, XREAL_1: 7;

      ( Im (((s * x) + (( 1r - s) * y)) .|. v)) = ( Im (((s * x) .|. v) + ((( 1r - s) * y) .|. v))) by CSSPACE:def 13

      .= ( Im ((s * (x .|. v)) + ((( 1r - s) * y) .|. v))) by CSSPACE:def 13

      .= ( Im ((s * (x .|. v)) + (( 1r - s) * (y .|. v)))) by CSSPACE:def 13

      .= (( Im (s * (x .|. v))) + ( Im (( 1r - s) * (y .|. v)))) by COMPLEX1: 8

      .= ((p * ( Im (x .|. v))) + ( Im (( 1r - s) * (y .|. v)))) by A6, Th43

      .= ((p * ( Im (x .|. v))) + ((1 - p) * ( Im (y .|. v)))) by A6, Th43;

      hence thesis by A1, A10;

    end;

    theorem :: CONVEX4:77

    for V be ComplexUnitarySpace-like non empty CUNITSTR, M be Subset of V, v be VECTOR of V, r be Real st M = { u where u be VECTOR of V : ( Im (u .|. v)) < r } holds M is convex

    proof

      let V be ComplexUnitarySpace-like non empty CUNITSTR;

      let M be Subset of V;

      let v be VECTOR of V;

      let r be Real;

      assume

       A1: M = { u where u be VECTOR of V : ( Im (u .|. v)) < r };

      let x,y be VECTOR of V;

      let s be Complex;

      assume that

       A2: ex p be Real st s = p & 0 < p & p < 1 and

       A3: x in M and

       A4: y in M;

      

       A5: ex u2 be VECTOR of V st y = u2 & ( Im (u2 .|. v)) < r by A1, A4;

      consider p be Real such that

       A6: s = p and

       A7: 0 < p and

       A8: p < 1 by A2;

      (1 - p) > 0 by A8, XREAL_1: 50;

      then

       A9: ((1 - p) * ( Im (y .|. v))) < ((1 - p) * r) by A5, XREAL_1: 68;

      ex u1 be VECTOR of V st x = u1 & ( Im (u1 .|. v)) < r by A1, A3;

      then (p * ( Im (x .|. v))) < (p * r) by A7, XREAL_1: 68;

      then

       A10: ((p * ( Im (x .|. v))) + ((1 - p) * ( Im (y .|. v)))) < ((p * r) + ((1 - p) * r)) by A9, XREAL_1: 8;

      ( Im (((s * x) + (( 1r - s) * y)) .|. v)) = ( Im (((s * x) .|. v) + ((( 1r - s) * y) .|. v))) by CSSPACE:def 13

      .= ( Im ((s * (x .|. v)) + ((( 1r - s) * y) .|. v))) by CSSPACE:def 13

      .= ( Im ((s * (x .|. v)) + (( 1r - s) * (y .|. v)))) by CSSPACE:def 13

      .= (( Im (s * (x .|. v))) + ( Im (( 1r - s) * (y .|. v)))) by COMPLEX1: 8

      .= ((p * ( Im (x .|. v))) + ( Im (( 1r - s) * (y .|. v)))) by A6, Th43

      .= ((p * ( Im (x .|. v))) + ((1 - p) * ( Im (y .|. v)))) by A6, Th43;

      hence thesis by A1, A10;

    end;

    theorem :: CONVEX4:78

    for V be ComplexUnitarySpace-like non empty CUNITSTR, M be Subset of V, v be VECTOR of V, r be Real st M = { u where u be VECTOR of V : |.(u .|. v).| <= r } holds M is convex

    proof

      let V be ComplexUnitarySpace-like non empty CUNITSTR;

      let M be Subset of V;

      let v be VECTOR of V;

      let r be Real;

      assume

       A1: M = { u where u be VECTOR of V : |.(u .|. v).| <= r };

      let x,y be VECTOR of V;

      let s be Complex;

      assume that

       A2: ex p be Real st s = p & 0 < p & p < 1 and

       A3: x in M and

       A4: y in M;

      consider p be Real such that

       A5: s = p and

       A6: 0 < p and

       A7: p < 1 by A2;

      

       A8: (1 - p) > 0 by A7, XREAL_1: 50;

      ex u2 be VECTOR of V st y = u2 & |.(u2 .|. v).| <= r by A1, A4;

      then

       A9: ((1 - p) * |.(y .|. v).|) <= ((1 - p) * r) by A8, XREAL_1: 64;

      ex u1 be VECTOR of V st x = u1 & |.(u1 .|. v).| <= r by A1, A3;

      then (p * |.(x .|. v).|) <= (p * r) by A6, XREAL_1: 64;

      then

       A10: ((p * |.(x .|. v).|) + ((1 - p) * |.(y .|. v).|)) <= ((p * r) + ((1 - p) * r)) by A9, XREAL_1: 7;

       |.(s * (x .|. v)).| = (p * |.(x .|. v).|) & |.(( 1r - s) * (y .|. v)).| = ((1 - p) * |.(y .|. v).|) by A5, A6, A7, Th44;

      then

       A11: |.((s * (x .|. v)) + (( 1r - s) * (y .|. v))).| <= ((p * |.(x .|. v).|) + ((1 - p) * |.(y .|. v).|)) by COMPLEX1: 56;

       |.(((s * x) + (( 1r - s) * y)) .|. v).| = |.(((s * x) .|. v) + ((( 1r - s) * y) .|. v)).| by CSSPACE:def 13

      .= |.((s * (x .|. v)) + ((( 1r - s) * y) .|. v)).| by CSSPACE:def 13

      .= |.((s * (x .|. v)) + (( 1r - s) * (y .|. v))).| by CSSPACE:def 13;

      then |.(((s * x) + (( 1r - s) * y)) .|. v).| <= r by A11, A10, XXREAL_0: 2;

      hence thesis by A1;

    end;

    theorem :: CONVEX4:79

    for V be ComplexUnitarySpace-like non empty CUNITSTR, M be Subset of V, v be VECTOR of V, r be Real st M = { u where u be VECTOR of V : |.(u .|. v).| < r } holds M is convex

    proof

      let V be ComplexUnitarySpace-like non empty CUNITSTR;

      let M be Subset of V;

      let v be VECTOR of V;

      let r be Real;

      assume

       A1: M = { u where u be VECTOR of V : |.(u .|. v).| < r };

      let x,y be VECTOR of V;

      let s be Complex;

      assume that

       A2: ex p be Real st s = p & 0 < p & p < 1 and

       A3: x in M and

       A4: y in M;

      consider p be Real such that

       A5: s = p and

       A6: 0 < p and

       A7: p < 1 by A2;

      

       A8: (1 - p) > 0 by A7, XREAL_1: 50;

      ex u2 be VECTOR of V st y = u2 & |.(u2 .|. v).| < r by A1, A4;

      then

       A9: ((1 - p) * |.(y .|. v).|) < ((1 - p) * r) by A8, XREAL_1: 68;

      ex u1 be VECTOR of V st x = u1 & |.(u1 .|. v).| < r by A1, A3;

      then (p * |.(x .|. v).|) < (p * r) by A6, XREAL_1: 68;

      then

       A10: ((p * |.(x .|. v).|) + ((1 - p) * |.(y .|. v).|)) < ((p * r) + ((1 - p) * r)) by A9, XREAL_1: 8;

       |.(s * (x .|. v)).| = (p * |.(x .|. v).|) & |.(( 1r - s) * (y .|. v)).| = ((1 - p) * |.(y .|. v).|) by A5, A6, A7, Th44;

      then

       A11: |.((s * (x .|. v)) + (( 1r - s) * (y .|. v))).| <= ((p * |.(x .|. v).|) + ((1 - p) * |.(y .|. v).|)) by COMPLEX1: 56;

       |.(((s * x) + (( 1r - s) * y)) .|. v).| = |.(((s * x) .|. v) + ((( 1r - s) * y) .|. v)).| by CSSPACE:def 13

      .= |.((s * (x .|. v)) + ((( 1r - s) * y) .|. v)).| by CSSPACE:def 13

      .= |.((s * (x .|. v)) + (( 1r - s) * (y .|. v))).| by CSSPACE:def 13;

      then |.(((s * x) + (( 1r - s) * y)) .|. v).| < r by A11, A10, XXREAL_0: 2;

      hence thesis by A1;

    end;

    begin

    definition

      let V be ComplexLinearSpace, L be C_Linear_Combination of V;

      :: CONVEX4:def24

      attr L is convex means 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 ;

    end

    theorem :: CONVEX4:80

    

     Th77: for V be ComplexLinearSpace, L be C_Linear_Combination of V st L is convex holds ( Carrier L) <> {}

    proof

      let V be ComplexLinearSpace;

      let L be C_Linear_Combination of V;

      assume L is convex;

      then

      consider F be FinSequence of the carrier of V such that

       A1: F is one-to-one & ( rng F) = ( Carrier L) and

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

      consider f be FinSequence of REAL such that

       A3: ( 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 A2;

      assume ( Carrier L) = {} ;

      then ( len F) = 0 by A1, CARD_1: 27, FINSEQ_4: 62;

      then f = ( <*> the carrier of V) by A3;

      hence contradiction by A3, RVSUM_1: 72;

    end;

    theorem :: CONVEX4:81

    for V be ComplexLinearSpace, L be C_Linear_Combination of V, v be VECTOR of V st L is convex & (ex r be Real st r = (L . v) & r <= 0 ) holds not v in ( Carrier L)

    proof

      let V be ComplexLinearSpace;

      let L be C_Linear_Combination of V;

      let v be VECTOR of V;

      assume that

       A1: L is convex and

       A2: ex r be Real st r = (L . v) & r <= 0 ;

      consider r be Real such that

       A3: r = (L . v) and

       A4: r <= 0 by A2;

      per cases by A4;

        suppose r = 0 ;

        hence thesis by A3, Th1;

      end;

        suppose

         A5: r < 0 ;

        now

          consider F be FinSequence of the carrier of V such that F is one-to-one and

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

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

          assume v in ( Carrier L);

          then

          consider n be object such that

           A8: n in ( dom F) and

           A9: (F . n) = v by A6, FUNCT_1:def 3;

          reconsider n as Element of NAT by A8;

          consider f be FinSequence of REAL such that

           A10: ( len f) = ( len F) and ( Sum f) = 1 and

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

          n in ( Seg ( len F)) by A8, FINSEQ_1:def 3;

          then

           A12: n in ( dom f) by A10, FINSEQ_1:def 3;

          then (L . v) = (f . n) by A11, A9;

          hence contradiction by A3, A5, A11, A12;

        end;

        hence thesis;

      end;

    end;

    theorem :: CONVEX4:82

    for V be ComplexLinearSpace, L be C_Linear_Combination of V st L is convex holds L <> ( ZeroCLC V)

    proof

      let V be ComplexLinearSpace;

      let L be C_Linear_Combination of V;

      assume L is convex;

      then

       A1: ( Carrier L) <> {} by Th77;

      assume L = ( ZeroCLC V);

      hence contradiction by A1;

    end;

    theorem :: CONVEX4:83

    

     Th80: for V be ComplexLinearSpace, v be VECTOR of V, L be C_Linear_Combination of V st L is convex & ( Carrier L) = {v} holds (ex r be Real st r = (L . v) & r = 1) & ( Sum L) = ((L . v) * v)

    proof

      let V be ComplexLinearSpace;

      let v be VECTOR of V;

      let L be C_Linear_Combination of V;

      assume that

       A1: L is convex and

       A2: ( Carrier L) = {v};

      reconsider L as C_Linear_Combination of {v} by A2, Def4;

      consider F be FinSequence of the carrier of V such that

       A3: F is one-to-one & ( rng F) = ( Carrier L) and

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

      

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

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

      reconsider r = (f /. 1) as Element of REAL ;

      ( card ( Carrier L)) = 1 by A2, CARD_1: 30;

      then ( len F) = 1 by A3, FINSEQ_4: 62;

      then

       A9: ( dom f) = ( Seg 1) by A6, FINSEQ_1:def 3;

      then

       A10: 1 in ( dom f);

      then

       A11: (f . 1) = (f /. 1) by PARTFUN1:def 6;

      then

       A12: f = <*r*> by A9, FINSEQ_1:def 8;

      (f . 1) = (L . (F . 1)) by A8, A10;

      then r = (L . v) by A11, A5, FINSEQ_1:def 8;

      hence thesis by A7, A12, Th14, FINSOP_1: 11;

    end;

    theorem :: CONVEX4:84

    

     Th81: for V be ComplexLinearSpace, v1,v2 be VECTOR of V, L be C_Linear_Combination of V st L is convex & ( Carrier L) = {v1, v2} & v1 <> v2 holds (ex r1,r2 be Real st r1 = (L . v1) & r2 = (L . v2) & (r1 + r2) = 1 & r1 >= 0 & r2 >= 0 ) & ( Sum L) = (((L . v1) * v1) + ((L . v2) * v2))

    proof

      let V be ComplexLinearSpace;

      let v1,v2 be VECTOR of V;

      let L be C_Linear_Combination of V;

      assume that

       A1: L is convex and

       A2: ( Carrier L) = {v1, v2} and

       A3: v1 <> v2;

      reconsider L as C_Linear_Combination of {v1, v2} by A2, Def4;

      consider F be FinSequence of the carrier of V such that

       A4: F is one-to-one & ( 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;

      ( len F) = ( card {v1, v2}) by A2, A4, FINSEQ_4: 62;

      then

       A9: ( len f) = 2 by A3, A6, CARD_2: 57;

      then

       A10: ( dom f) = {1, 2} by FINSEQ_1: 2, FINSEQ_1:def 3;

      then

       A11: 2 in ( dom f) by TARSKI:def 2;

      then

       A12: (f . 2) = (L . (F . 2)) by A8;

      then (f /. 2) = (L . (F . 2)) by A11, PARTFUN1:def 6;

      then

      reconsider r2 = (L . (F . 2)) as Real;

      

       A13: (f . 2) >= 0 by A8, A11;

      

       A14: 1 in ( dom f) by A10, TARSKI:def 2;

      then

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

      then (f /. 1) = (L . (F . 1)) by A14, PARTFUN1:def 6;

      then

      reconsider r1 = (L . (F . 1)) as Real;

      

       A16: f = <*r1, r2*> by A9, A15, A12, FINSEQ_1: 44;

      ex c1,c2 be Real st c1 = (L . v1) & c2 = (L . v2) & (c1 + c2) = 1 & c1 >= 0 & c2 >= 0

      proof

        per cases by A2, A3, A4, FINSEQ_3: 99;

          suppose F = <*v1, v2*>;

          then

           A17: r1 = (L . v1) & r2 = (L . v2) by FINSEQ_1: 44;

          (r1 + r2) = 1 & r1 >= 0 by A7, A8, A14, A15, A16, RVSUM_1: 77;

          hence thesis by A12, A13, A17;

        end;

          suppose F = <*v2, v1*>;

          then

           A18: r1 = (L . v2) & r2 = (L . v1) by FINSEQ_1: 44;

          (r1 + r2) = 1 & r1 >= 0 by A7, A8, A14, A15, A16, RVSUM_1: 77;

          hence thesis by A12, A13, A18;

        end;

      end;

      hence thesis by A3, Th15;

    end;

    

     Lm3: for V be ComplexLinearSpace, v1,v2,v3 be VECTOR of V, L be C_Linear_Combination of {v1, v2, v3} st v1 <> v2 & v2 <> v3 & v3 <> v1 holds ( Sum L) = ((((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3))

    proof

      let V be ComplexLinearSpace;

      let v1,v2,v3 be VECTOR of V;

      let L be C_Linear_Combination of {v1, v2, v3};

      assume that

       A1: v1 <> v2 and

       A2: v2 <> v3 and

       A3: v3 <> v1;

      

       A4: ( Carrier L) c= {v1, v2, v3} by Def4;

      per cases by A4, ZFMISC_1: 118;

        suppose ( Carrier L) = {} ;

        then

         A5: L = ( ZeroCLC V) by Def3;

        

        then ( Sum L) = ( 0. V) by Th11

        .= (( 0. V) + ( 0. V))

        .= ((( 0. V) + ( 0. V)) + ( 0. V))

        .= ((( 0c * v1) + ( 0. V)) + ( 0. V)) by CLVECT_1: 1

        .= ((( 0c * v1) + ( 0c * v2)) + ( 0. V)) by CLVECT_1: 1

        .= ((( 0c * v1) + ( 0c * v2)) + ( 0c * v3)) by CLVECT_1: 1

        .= ((((L . v1) * v1) + ( 0c * v2)) + ( 0c * v3)) by A5, Th2

        .= ((((L . v1) * v1) + ((L . v2) * v2)) + ( 0c * v3)) by A5, Th2

        .= ((((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)) by A5, Th2;

        hence thesis;

      end;

        suppose

         A6: ( Carrier L) = {v1};

        then

        reconsider L as C_Linear_Combination of {v1} by Def4;

        

         A7: not v2 in ( Carrier L) by A1, A6, TARSKI:def 1;

        

         A8: not v3 in ( Carrier L) by A3, A6, TARSKI:def 1;

        ( Sum L) = ((L . v1) * v1) by Th14

        .= (((L . v1) * v1) + ( 0. V))

        .= ((((L . v1) * v1) + ( 0. V)) + ( 0. V))

        .= ((((L . v1) * v1) + ( 0c * v2)) + ( 0. V)) by CLVECT_1: 1

        .= ((((L . v1) * v1) + ( 0c * v2)) + ( 0c * v3)) by CLVECT_1: 1

        .= ((((L . v1) * v1) + ((L . v2) * v2)) + ( 0c * v3)) by A7

        .= ((((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)) by A8;

        hence thesis;

      end;

        suppose

         A9: ( Carrier L) = {v2};

        then

        reconsider L as C_Linear_Combination of {v2} by Def4;

        

         A10: not v1 in ( Carrier L) by A1, A9, TARSKI:def 1;

        

         A11: not v3 in ( Carrier L) by A2, A9, TARSKI:def 1;

        ( Sum L) = ((L . v2) * v2) by Th14

        .= (( 0. V) + ((L . v2) * v2))

        .= ((( 0. V) + ((L . v2) * v2)) + ( 0. V))

        .= ((( 0c * v1) + ((L . v2) * v2)) + ( 0. V)) by CLVECT_1: 1

        .= ((( 0c * v1) + ((L . v2) * v2)) + ( 0c * v3)) by CLVECT_1: 1

        .= ((((L . v1) * v1) + ((L . v2) * v2)) + ( 0c * v3)) by A10

        .= ((((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)) by A11;

        hence thesis;

      end;

        suppose

         A12: ( Carrier L) = {v3};

        then

        reconsider L as C_Linear_Combination of {v3} by Def4;

        

         A13: not v1 in ( Carrier L) by A3, A12, TARSKI:def 1;

        

         A14: not v2 in ( Carrier L) by A2, A12, TARSKI:def 1;

        ( Sum L) = ((L . v3) * v3) by Th14

        .= (( 0. V) + ((L . v3) * v3))

        .= ((( 0. V) + ( 0. V)) + ((L . v3) * v3))

        .= ((( 0c * v1) + ( 0. V)) + ((L . v3) * v3)) by CLVECT_1: 1

        .= ((( 0c * v1) + ( 0c * v2)) + ((L . v3) * v3)) by CLVECT_1: 1

        .= ((((L . v1) * v1) + ( 0c * v2)) + ((L . v3) * v3)) by A13

        .= ((((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)) by A14;

        hence thesis;

      end;

        suppose

         A15: ( Carrier L) = {v1, v2};

        

        then

         A16: ( Sum L) = (((L . v1) * v1) + ((L . v2) * v2)) by A1, Th18

        .= ((((L . v1) * v1) + ((L . v2) * v2)) + ( 0. V))

        .= ((((L . v1) * v1) + ((L . v2) * v2)) + ( 0c * v3)) by CLVECT_1: 1;

         not v3 in ( Carrier L) by A2, A3, A15, TARSKI:def 2;

        hence thesis by A16;

      end;

        suppose

         A17: ( Carrier L) = {v1, v3};

        

        then

         A18: ( Sum L) = (((L . v1) * v1) + ((L . v3) * v3)) by A3, Th18

        .= ((((L . v1) * v1) + ( 0. V)) + ((L . v3) * v3))

        .= ((((L . v1) * v1) + ( 0c * v2)) + ((L . v3) * v3)) by CLVECT_1: 1;

         not v2 in ( Carrier L) by A1, A2, A17, TARSKI:def 2;

        hence thesis by A18;

      end;

        suppose

         A19: ( Carrier L) = {v2, v3};

        

        then

         A20: ( Sum L) = (((L . v2) * v2) + ((L . v3) * v3)) by A2, Th18

        .= ((( 0. V) + ((L . v2) * v2)) + ((L . v3) * v3))

        .= ((( 0c * v1) + ((L . v2) * v2)) + ((L . v3) * v3)) by CLVECT_1: 1;

         not v1 in ( Carrier L) by A1, A3, A19, TARSKI:def 2;

        hence thesis by A20;

      end;

        suppose ( Carrier L) = {v1, v2, v3};

        then

        consider F be FinSequence of the carrier of V such that

         A21: F is one-to-one & ( rng F) = {v1, v2, v3} and

         A22: ( Sum L) = ( Sum (L (#) F)) by Def6;

        F = <*v1, v2, v3*> or F = <*v1, v3, v2*> or F = <*v2, v1, v3*> or F = <*v2, v3, v1*> or F = <*v3, v1, v2*> or F = <*v3, v2, v1*> by A1, A2, A3, A21, CONVEX1: 31;

        then (L (#) F) = <*((L . v1) * v1), ((L . v2) * v2), ((L . v3) * v3)*> or (L (#) F) = <*((L . v1) * v1), ((L . v3) * v3), ((L . v2) * v2)*> or (L (#) F) = <*((L . v2) * v2), ((L . v1) * v1), ((L . v3) * v3)*> or (L (#) F) = <*((L . v2) * v2), ((L . v3) * v3), ((L . v1) * v1)*> or (L (#) F) = <*((L . v3) * v3), ((L . v1) * v1), ((L . v2) * v2)*> or (L (#) F) = <*((L . v3) * v3), ((L . v2) * v2), ((L . v1) * v1)*> by Th10;

        then ( Sum L) = ((((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)) or ( Sum L) = (((L . v1) * v1) + (((L . v2) * v2) + ((L . v3) * v3))) or ( Sum L) = (((L . v2) * v2) + (((L . v1) * v1) + ((L . v3) * v3))) by A22, RLVECT_1: 46;

        hence thesis by RLVECT_1:def 3;

      end;

    end;

    theorem :: CONVEX4:85

    

     Th82: for V be ComplexLinearSpace, v1,v2,v3 be VECTOR of V, L be C_Linear_Combination of V st L is convex & ( Carrier L) = {v1, v2, v3} & v1 <> v2 & v2 <> v3 & v3 <> v1 holds (ex r1,r2,r3 be Real st r1 = (L . v1) & r2 = (L . v2) & r3 = (L . v3) & ((r1 + r2) + r3) = 1 & r1 >= 0 & r2 >= 0 & r3 >= 0 ) & ( Sum L) = ((((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3))

    proof

      let V be ComplexLinearSpace;

      let v1,v2,v3 be VECTOR of V;

      let L be C_Linear_Combination of V;

      assume that

       A1: L is convex and

       A2: ( Carrier L) = {v1, v2, v3} and

       A3: v1 <> v2 & v2 <> v3 & v3 <> v1;

      reconsider L as C_Linear_Combination of {v1, v2, v3} by A2, Def4;

      consider F be FinSequence of the carrier of V such that

       A4: F is one-to-one & ( 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;

      ( len F) = ( card {v1, v2, v3}) by A2, A4, FINSEQ_4: 62;

      then

       A9: ( len f) = 3 by A3, A6, CARD_2: 58;

      then

       A10: ( dom f) = {1, 2, 3} by FINSEQ_1:def 3, FINSEQ_3: 1;

      then

       A11: 2 in ( dom f) by ENUMSET1:def 1;

      then

       A12: (f . 2) = (L . (F . 2)) by A8;

      then (f /. 2) = (L . (F . 2)) by A11, PARTFUN1:def 6;

      then

      reconsider r2 = (L . (F . 2)) as Element of REAL ;

      

       A13: (f . 2) >= 0 by A8, A11;

      

       A14: 3 in ( dom f) by A10, ENUMSET1:def 1;

      then

       A15: (f . 3) = (L . (F . 3)) by A8;

      then (f /. 3) = (L . (F . 3)) by A14, PARTFUN1:def 6;

      then

      reconsider r3 = (L . (F . 3)) as Element of REAL ;

      

       A16: (f . 3) >= 0 by A8, A14;

      

       A17: 1 in ( dom f) by A10, ENUMSET1:def 1;

      then

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

      then (f /. 1) = (L . (F . 1)) by A17, PARTFUN1:def 6;

      then

      reconsider r1 = (L . (F . 1)) as Element of REAL ;

      

       A19: f = <*r1, r2, r3*> by A9, A18, A12, A15, FINSEQ_1: 45;

      then

       A20: ((r1 + r2) + r3) = 1 by A7, RVSUM_1: 78;

      

       A21: (f . 1) >= 0 by A8, A17;

      ex a,b,c be Real st a = (L . v1) & b = (L . v2) & c = (L . v3) & ((a + b) + c) = 1 & a >= 0 & b >= 0 & c >= 0

      proof

        per cases by A2, A3, A4, CONVEX1: 31;

          suppose

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

          then

           A23: r1 = (L . v1) & r2 = (L . v2) by FINSEQ_1: 45;

          

           A24: r2 >= 0 by A8, A11, A12;

          

           A25: r3 = (L . v3) by A22, FINSEQ_1: 45;

          ((r1 + r2) + r3) = 1 & r1 >= 0 by A7, A8, A17, A18, A19, RVSUM_1: 78;

          hence thesis by A15, A16, A23, A25, A24;

        end;

          suppose

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

          then

           A27: r1 = (L . v1) & r3 = (L . v2) by FINSEQ_1: 45;

          

           A28: r3 >= 0 by A8, A14, A15;

          

           A29: r2 = (L . v3) by A26, FINSEQ_1: 45;

          ((r1 + r3) + r2) = 1 & r1 >= 0 by A8, A17, A18, A20;

          hence thesis by A12, A13, A27, A29, A28;

        end;

          suppose

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

          then

           A31: r2 = (L . v1) & r1 = (L . v2) by FINSEQ_1: 45;

          

           A32: r1 >= 0 by A8, A17, A18;

          

           A33: r3 = (L . v3) by A30, FINSEQ_1: 45;

          ((r2 + r1) + r3) = 1 & r2 >= 0 by A7, A8, A11, A12, A19, RVSUM_1: 78;

          hence thesis by A15, A16, A31, A33, A32;

        end;

          suppose

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

          then

           A35: r3 = (L . v1) & r1 = (L . v2) by FINSEQ_1: 45;

          

           A36: r1 >= 0 by A8, A17, A18;

          

           A37: r2 = (L . v3) by A34, FINSEQ_1: 45;

          ((r3 + r1) + r2) = 1 & r3 >= 0 by A8, A14, A15, A20;

          hence thesis by A12, A13, A35, A37, A36;

        end;

          suppose

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

          then

           A39: r2 = (L . v1) & r3 = (L . v2) by FINSEQ_1: 45;

          

           A40: r3 >= 0 by A8, A14, A15;

          

           A41: r1 = (L . v3) by A38, FINSEQ_1: 45;

          ((r2 + r3) + r1) = 1 & r2 >= 0 by A8, A11, A12, A20;

          hence thesis by A18, A21, A39, A41, A40;

        end;

          suppose

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

          then

           A43: r3 = (L . v1) & r2 = (L . v2) by FINSEQ_1: 45;

          

           A44: r2 >= 0 by A8, A11, A12;

          

           A45: r1 = (L . v3) by A42, FINSEQ_1: 45;

          ((r3 + r2) + r1) = 1 & r3 >= 0 by A8, A14, A15, A20;

          hence thesis by A18, A21, A43, A45, A44;

        end;

      end;

      hence thesis by A3, Lm3;

    end;

    theorem :: CONVEX4:86

    for V be ComplexLinearSpace, v be VECTOR of V, L be C_Linear_Combination of {v} st L is convex holds (ex r be Real st r = (L . v) & r = 1) & ( Sum L) = ((L . v) * v)

    proof

      let V be ComplexLinearSpace;

      let v be VECTOR of V;

      let L be C_Linear_Combination of {v};

      ( Carrier L) c= {v} by Def4;

      then

       A1: ( Carrier L) = {} or ( Carrier L) = {v} by ZFMISC_1: 33;

      assume L is convex;

      hence thesis by A1, Th77, Th80;

    end;

    theorem :: CONVEX4:87

    for V be ComplexLinearSpace, v1,v2 be VECTOR of V, L be C_Linear_Combination of {v1, v2} st v1 <> v2 & L is convex holds (ex r1,r2 be Real st r1 = (L . v1) & r2 = (L . v2) & r1 >= 0 & r2 >= 0 ) & ( Sum L) = (((L . v1) * v1) + ((L . v2) * v2))

    proof

      let V be ComplexLinearSpace;

      let v1,v2 be VECTOR of V;

      let L be C_Linear_Combination of {v1, v2};

      assume that

       A1: v1 <> v2 and

       A2: L is convex;

      

       A3: ( Carrier L) c= {v1, v2} by Def4;

      

       A4: ( Carrier L) <> {} by A2, Th77;

      ex r1,r2 be Real st r1 = (L . v1) & r2 = (L . v2) & r1 >= 0 & r2 >= 0

      proof

        per cases by A3, A4, ZFMISC_1: 36;

          suppose

           A5: ( Carrier L) = {v1};

          then not v2 in ( Carrier L) by A1, TARSKI:def 1;

          then

           A6: 0 = (L . v2);

          ex r be Real st r = (L . v1) & r = 1 by A2, A5, Th80;

          hence thesis by A6;

        end;

          suppose

           A7: ( Carrier L) = {v2};

          then not v1 in ( Carrier L) by A1, TARSKI:def 1;

          then

           A8: 0 = (L . v1);

          ex r be Real st r = (L . v2) & r = 1 by A2, A7, Th80;

          hence thesis by A8;

        end;

          suppose ( Carrier L) = {v1, v2};

          then ex r1,r2 be Real st r1 = (L . v1) & r2 = (L . v2) & (r1 + r2) = 1 & r1 >= 0 & r2 >= 0 by A1, A2, Th81;

          hence thesis;

        end;

      end;

      hence thesis by A1, Th15;

    end;

    theorem :: CONVEX4:88

    for V be ComplexLinearSpace, v1,v2,v3 be VECTOR of V, L be C_Linear_Combination of {v1, v2, v3} st v1 <> v2 & v2 <> v3 & v3 <> v1 & L is convex holds (ex r1,r2,r3 be Real st r1 = (L . v1) & r2 = (L . v2) & r3 = (L . v3) & ((r1 + r2) + r3) = 1 & r1 >= 0 & r2 >= 0 & r3 >= 0 ) & ( Sum L) = ((((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3))

    proof

      let V be ComplexLinearSpace;

      let v1,v2,v3 be VECTOR of V;

      let L be C_Linear_Combination of {v1, v2, v3};

      assume that

       A1: v1 <> v2 and

       A2: v2 <> v3 and

       A3: v3 <> v1 and

       A4: L is convex;

      

       A5: ( Carrier L) c= {v1, v2, v3} by Def4;

      

       A6: ( Carrier L) <> {} by A4, Th77;

      ex r1,r2,r3 be Real st r1 = (L . v1) & r2 = (L . v2) & r3 = (L . v3) & ((r1 + r2) + r3) = 1 & r1 >= 0 & r2 >= 0 & r3 >= 0

      proof

        per cases by A5, A6, ZFMISC_1: 118;

          suppose

           A7: ( Carrier L) = {v1};

          then not v2 in ( Carrier L) by A1, TARSKI:def 1;

          then

           A8: 0 = (L . v2);

          

           A9: ((1 + 0 ) + 0 ) = 1;

           not v3 in ( Carrier L) by A3, A7, TARSKI:def 1;

          then

           A10: 0 = (L . v3);

          ex r be Real st r = (L . v1) & r = 1 by A4, A7, Th80;

          hence thesis by A8, A10, A9;

        end;

          suppose

           A11: ( Carrier L) = {v2};

          then not v1 in ( Carrier L) by A1, TARSKI:def 1;

          then

           A12: 0 = (L . v1);

          

           A13: (( 0 + 1) + 0 ) = 1;

           not v3 in ( Carrier L) by A2, A11, TARSKI:def 1;

          then

           A14: 0 = (L . v3);

          ex r be Real st r = (L . v2) & r = 1 by A4, A11, Th80;

          hence thesis by A12, A14, A13;

        end;

          suppose

           A15: ( Carrier L) = {v3};

          then not v1 in ( Carrier L) by A3, TARSKI:def 1;

          then

           A16: 0 = (L . v1);

          

           A17: (( 0 + 0 ) + 1) = 1;

           not v2 in ( Carrier L) by A2, A15, TARSKI:def 1;

          then

           A18: 0 = (L . v2);

          ex r be Real st r = (L . v3) & r = 1 by A4, A15, Th80;

          hence thesis by A16, A18, A17;

        end;

          suppose

           A19: ( Carrier L) = {v1, v2};

          set r3 = 0 ;

           not v3 in { v where v be Element of V : (L . v) <> 0 } by A2, A3, A19, TARSKI:def 2;

          then

           A20: r3 = (L . v3);

          consider r1,r2 be Real such that

           A21: r1 = (L . v1) & r2 = (L . v2) and

           A22: (r1 + r2) = 1 and

           A23: r1 >= 0 & r2 >= 0 by A1, A4, A19, Th81;

          ((r1 + r2) + r3) = 1 by A22;

          hence thesis by A21, A23, A20;

        end;

          suppose

           A24: ( Carrier L) = {v2, v3};

          set r1 = 0 ;

           not v1 in ( Carrier L) by A1, A3, A24, TARSKI:def 2;

          then

           A25: r1 = (L . v1);

          consider r2,r3 be Real such that

           A26: r2 = (L . v2) & r3 = (L . v3) and

           A27: (r2 + r3) = 1 and

           A28: r2 >= 0 & r3 >= 0 by A2, A4, A24, Th81;

          ((r1 + r2) + r3) = 1 by A27;

          hence thesis by A26, A28, A25;

        end;

          suppose

           A29: ( Carrier L) = {v1, v3};

          set r2 = 0 ;

           not v2 in ( Carrier L) by A1, A2, A29, TARSKI:def 2;

          then

           A30: r2 = (L . v2);

          consider r1,r3 be Real such that

           A31: r1 = (L . v1) & r3 = (L . v3) and

           A32: (r1 + r3) = 1 and

           A33: r1 >= 0 & r3 >= 0 by A3, A4, A29, Th81;

          ((r1 + r2) + r3) = 1 by A32;

          hence thesis by A31, A33, A30;

        end;

          suppose ( Carrier L) = {v1, v2, v3};

          hence thesis by A1, A2, A3, A4, Th82;

        end;

      end;

      hence thesis by A1, A2, A3, Lm3;

    end;

    begin

    definition

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

      :: CONVEX4:def25

      func Convex-Family M -> Subset-Family of V means

      : Def25: for N be Subset of V holds N in it iff N is convex & M c= N;

      existence

      proof

        defpred P[ Subset of V] means $1 is convex & M c= $1;

        thus ex F be Subset-Family of V st for N be Subset of V holds N in F iff P[N] from SUBSET_1:sch 3;

      end;

      uniqueness

      proof

        let SF,SG be Subset-Family of V;

        assume that

         A1: for N be Subset of V holds N in SF iff N is convex & M c= N and

         A2: for N be Subset of V holds N in SG iff N is convex & M c= N;

        for Y be Subset of V holds Y in SF iff Y in SG

        proof

          let Y be Subset of V;

          hereby

            assume Y in SF;

            then Y is convex & M c= Y by A1;

            hence Y in SG by A2;

          end;

          assume Y in SG;

          then Y is convex & M c= Y by A2;

          hence thesis by A1;

        end;

        hence thesis by SETFAM_1: 31;

      end;

    end

    definition

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

      :: CONVEX4:def26

      func conv M -> convex Subset of V equals ( meet ( Convex-Family M));

      coherence

      proof

        for N be Subset of V st N in ( Convex-Family M) holds N is convex by Def25;

        hence thesis by Th65;

      end;

    end

    theorem :: CONVEX4:89

    for V be non empty CLSStruct, M be Subset of V, N be convex Subset of V st M c= N holds ( conv M) c= N

    proof

      let V be non empty CLSStruct;

      let M be Subset of V;

      let N be convex Subset of V;

      assume M c= N;

      then N in ( Convex-Family M) by Def25;

      hence thesis by SETFAM_1: 3;

    end;