circled1.miz



    begin

    

     Lm1: for V be non empty RLSStruct, M,N be Subset of V, x,y be VECTOR of V st x in M & y in N holds (x - y) in (M - N)

    proof

      let V be non empty RLSStruct, M,N be Subset of V, x,y be VECTOR of V;

      (M - N) = { (u - v) where u,v be VECTOR of V : u in M & v in N } by RUSUB_5:def 2;

      hence thesis;

    end;

    theorem :: CIRCLED1:1

    

     Th1: for V be RealLinearSpace, A,B be circled Subset of V holds (A - B) is circled

    proof

      let V be RealLinearSpace, A,B be circled Subset of V;

      

       A1: (A - B) = { (u - v) where u,v be VECTOR of V : u in A & v in B } by RUSUB_5:def 2;

      let r be Real;

      assume |.r.| <= 1;

      then

       A2: (r * A) c= A & (r * B) c= B by RLTOPSP1:def 6;

      let x be object;

      assume

       A3: x in (r * (A - B));

      (r * (A - B)) = { (r * v) where v be VECTOR of V : v in (A - B) } by CONVEX1:def 1;

      then

      consider x9 be VECTOR of V such that

       A4: x = (r * x9) and

       A5: x9 in (A - B) by A3;

      consider u,v be VECTOR of V such that

       A6: x9 = (u - v) and

       A7: u in A & v in B by A1, A5;

      reconsider r as Real;

      

       A8: (r * u) in (r * A) & (r * v) in (r * B) by A7, RLTOPSP1: 1;

      x = ((r * u) - (r * v)) by A4, A6, RLVECT_1: 34;

      hence thesis by A2, A8, Lm1;

    end;

    registration

      let V be RealLinearSpace, M,N be circled Subset of V;

      cluster (M - N) -> circled;

      coherence by Th1;

    end

    definition

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

      :: original: circled

      redefine

      :: CIRCLED1:def1

      attr M is circled means

      : Def1: for u be VECTOR of V, r be Real st |.r.| <= 1 & u in M holds (r * u) in M;

      compatibility

      proof

        thus M is circled implies for u be VECTOR of V, r be Real st |.r.| <= 1 & u in M holds (r * u) in M

        proof

          assume

           A1: M is circled;

          let u be VECTOR of V, r be Real;

          assume |.r.| <= 1;

          then

           A2: (r * M) c= M by A1;

          assume u in M;

          then (r * u) in (r * M) by RLTOPSP1: 1;

          hence thesis by A2;

        end;

        assume

         A3: for u be VECTOR of V, r be Real st |.r.| <= 1 & u in M holds (r * u) in M;

        let r be Real;

        assume

         A4: |.r.| <= 1;

        reconsider r as Real;

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

        proof

          let x be Element of V;

          assume x in (r * M);

          then

          consider u be Element of V such that

           A5: x = u and

           A6: u in (r * M);

          u in { (r * w) where w be Element of V : w in M } by A6, CONVEX1:def 1;

          then ex w1 be Element of V st u = (r * w1) & w1 in M;

          hence thesis by A3, A4, A5;

        end;

        hence thesis;

      end;

    end

    theorem :: CIRCLED1:2

    

     Th2: for V be RealLinearSpace, M be Subset of V, r be Real st M is circled holds (r * M) is circled

    proof

      let V be RealLinearSpace, M be Subset of V, r be Real;

      assume

       A1: M is circled;

      for u be VECTOR of V, p be Real st |.p.| <= 1 & u in (r * M) holds (p * u) in (r * M)

      proof

        let u be VECTOR of V, p be Real;

        assume that

         A2: |.p.| <= 1 and

         A3: u in (r * M);

        u in { (r * w) where w be Element of V : w in M } by A3, CONVEX1:def 1;

        then

        consider u9 be Element of V such that

         A4: u = (r * u9) and

         A5: u9 in M;

        

         A6: (p * u) = ((r * p) * u9) by A4, RLVECT_1:def 7

        .= (r * (p * u9)) by RLVECT_1:def 7;

        (p * u9) in M by A1, A2, A5;

        hence thesis by A6, RLTOPSP1: 1;

      end;

      hence thesis;

    end;

    theorem :: CIRCLED1:3

    

     Th3: for V be RealLinearSpace, M1,M2 be Subset of V, r1,r2 be Real st M1 is circled & M2 is circled holds ((r1 * M1) + (r2 * M2)) is circled

    proof

      let V be RealLinearSpace, M1,M2 be Subset of V, r1,r2 be Real;

      assume that

       A1: M1 is circled and

       A2: M2 is circled;

      let u be VECTOR of V, p be Real;

      assume that

       A3: |.p.| <= 1 and

       A4: u in ((r1 * M1) + (r2 * M2));

      u in { (x + y) where x,y be VECTOR of V : x in (r1 * M1) & y in (r2 * M2) } by A4, RUSUB_4:def 9;

      then

      consider u1,u2 be VECTOR of V such that

       A5: u = (u1 + u2) and

       A6: u1 in (r1 * M1) and

       A7: u2 in (r2 * M2);

      u1 in { (r1 * x) where x be VECTOR of V : x in M1 } by A6, CONVEX1:def 1;

      then

      consider x1 be VECTOR of V such that

       A8: u1 = (r1 * x1) and

       A9: x1 in M1;

      

       A10: (p * u1) = ((r1 * p) * x1) by A8, RLVECT_1:def 7

      .= (r1 * (p * x1)) by RLVECT_1:def 7;

      u2 in { (r2 * x) where x be VECTOR of V : x in M2 } by A7, CONVEX1:def 1;

      then

      consider x2 be VECTOR of V such that

       A11: u2 = (r2 * x2) and

       A12: x2 in M2;

      

       A13: (p * u2) = ((r2 * p) * x2) by A11, RLVECT_1:def 7

      .= (r2 * (p * x2)) by RLVECT_1:def 7;

      reconsider r1, r2 as Real;

      (p * x2) in M2 by A2, A3, A12;

      then

       A14: (p * u2) in (r2 * M2) by A13, RLTOPSP1: 1;

      (p * x1) in M1 by A1, A3, A9;

      then

       A15: (p * u1) in (r1 * M1) by A10, RLTOPSP1: 1;

      (p * (u1 + u2)) = ((p * u1) + (p * u2)) by RLVECT_1:def 5;

      then (p * (u1 + u2)) in { (x + y) where x,y be VECTOR of V : x in (r1 * M1) & y in (r2 * M2) } by A15, A14;

      hence thesis by A5, RUSUB_4:def 9;

    end;

    theorem :: CIRCLED1:4

    for V be RealLinearSpace, M1,M2,M3 be Subset of V, r1,r2,r3 be Real st M1 is circled & M2 is circled & M3 is circled holds (((r1 * M1) + (r2 * M2)) + (r3 * M3)) is circled

    proof

      let V be RealLinearSpace, M1,M2,M3 be Subset of V, r1,r2,r3 be Real;

      assume that

       A1: M1 is circled & M2 is circled and

       A2: M3 is circled;

      ((r1 * M1) + (r2 * M2)) is circled by A1, Th3;

      then ((1 * ((r1 * M1) + (r2 * M2))) + (r3 * M3)) is circled by A2, Th3;

      hence thesis by CONVEX1: 32;

    end;

    theorem :: CIRCLED1:5

    for V be RealLinearSpace holds ( Up ( (0). V)) is circled

    proof

      let V be RealLinearSpace, u be VECTOR of V, r be Real;

      assume that |.r.| <= 1 and

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

      u in the carrier of ( (0). V) by A1, RUSUB_4:def 5;

      then u in {( 0. V)} by RLSUB_1:def 3;

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

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

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

      then (r * u) in the carrier of ( (0). V) by RLSUB_1:def 3;

      hence thesis by RUSUB_4:def 5;

    end;

    theorem :: CIRCLED1:6

    

     Th6: for V be RealLinearSpace holds ( Up ( (Omega). V)) is circled

    proof

      let V be RealLinearSpace, u be VECTOR of V, r be Real;

      ( (Omega). V) = the RLSStruct of V by RLSUB_1:def 4;

      then (r * u) in the carrier of ( (Omega). V);

      hence thesis by RUSUB_4:def 5;

    end;

    theorem :: CIRCLED1:7

    for V be RealLinearSpace, M,N be circled Subset of V holds (M /\ N) is circled

    proof

      let V be RealLinearSpace, M,N be circled Subset of V, x be VECTOR of V, r be Real;

      assume that

       A1: |.r.| <= 1 and

       A2: x in (M /\ N);

      x in N by A2, XBOOLE_0:def 4;

      then

       A3: (r * x) in N by A1, Def1;

      x in M by A2, XBOOLE_0:def 4;

      then (r * x) in M by A1, Def1;

      hence thesis by A3, XBOOLE_0:def 4;

    end;

    theorem :: CIRCLED1:8

    for V be RealLinearSpace, M,N be circled Subset of V holds (M \/ N) is circled

    proof

      let V be RealLinearSpace, M,N be circled Subset of V, x be VECTOR of V, r be Real;

      assume that

       A1: |.r.| <= 1 and

       A2: x in (M \/ N);

      x in M or x in N by A2, XBOOLE_0:def 3;

      then (r * x) in M or (r * x) in N by A1, Def1;

      hence thesis by XBOOLE_0:def 3;

    end;

    begin

    definition

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

      :: CIRCLED1:def2

      func Circled-Family M -> Subset-Family of V means

      : Def2: for N be Subset of V holds N in it iff N is circled & M c= N;

      existence

      proof

        defpred P[ Subset of V] means $1 is circled & 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 circled & M c= N and

         A2: for N be Subset of V holds N in SG iff N is circled & 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 circled & M c= Y by A1;

            hence Y in SG by A2;

          end;

          assume Y in SG;

          then Y is circled & M c= Y by A2;

          hence thesis by A1;

        end;

        hence thesis by SETFAM_1: 31;

      end;

    end

    definition

      let V be RealLinearSpace, M be Subset of V;

      :: CIRCLED1:def3

      func Cir M -> circled Subset of V equals ( meet ( Circled-Family M));

      coherence

      proof

        for N be Subset of V st N in ( Circled-Family M) holds N is circled by Def2;

        then ( Circled-Family M) is circled-membered;

        hence thesis by RLTOPSP1: 30;

      end;

    end

    registration

      let V be RealLinearSpace, M be Subset of V;

      cluster ( Circled-Family M) -> non empty;

      coherence

      proof

        

         A1: M c= ( Up ( (Omega). V))

        proof

          let u be object;

          assume u in M;

          then

          reconsider u as Element of V;

          u in the carrier of the RLSStruct of V;

          then u in the carrier of ( (Omega). V) by RLSUB_1:def 4;

          hence thesis by RUSUB_4:def 5;

        end;

        ( Up ( (Omega). V)) is circled by Th6;

        hence thesis by A1, Def2;

      end;

    end

    theorem :: CIRCLED1:9

    

     Th9: for V be RealLinearSpace, M1,M2 be Subset of V st M1 c= M2 holds ( Circled-Family M2) c= ( Circled-Family M1)

    proof

      let V be RealLinearSpace, M1,M2 be Subset of V such that

       A1: M1 c= M2;

      let M be object;

      assume

       A2: M in ( Circled-Family M2);

      then

      reconsider M as Subset of V;

      M2 c= M by A2, Def2;

      then

       A3: M1 c= M by A1;

      M is circled by A2, Def2;

      hence thesis by A3, Def2;

    end;

    theorem :: CIRCLED1:10

    for V be RealLinearSpace, M1,M2 be Subset of V st M1 c= M2 holds ( Cir M1) c= ( Cir M2)

    proof

      let V be RealLinearSpace, M1,M2 be Subset of V;

      assume M1 c= M2;

      then ( Circled-Family M2) c= ( Circled-Family M1) by Th9;

      then

       A1: ( meet ( Circled-Family M1)) c= ( meet ( Circled-Family M2)) by SETFAM_1: 6;

      let x be object;

      assume x in ( Cir M1);

      hence thesis by A1;

    end;

    theorem :: CIRCLED1:11

    

     Th11: for V be RealLinearSpace, M be Subset of V holds M c= ( Cir M)

    proof

      let V be RealLinearSpace, M be Subset of V, u be object;

      assume

       A1: u in M;

      for Y be set holds Y in ( Circled-Family M) implies u in Y

      proof

        let Y be set;

        assume

         A2: Y in ( Circled-Family M);

        then

        reconsider Y as Subset of V;

        M c= Y by A2, Def2;

        hence thesis by A1;

      end;

      hence thesis by SETFAM_1:def 1;

    end;

    theorem :: CIRCLED1:12

    

     Th12: for V be RealLinearSpace, M be Subset of V, N be circled Subset of V st M c= N holds ( Cir M) c= N

    proof

      let V be RealLinearSpace, M be Subset of V, N be circled Subset of V;

      assume M c= N;

      then N in ( Circled-Family M) by Def2;

      hence thesis by SETFAM_1: 3;

    end;

    theorem :: CIRCLED1:13

    for V be RealLinearSpace, M be circled Subset of V holds ( Cir M) = M by Th12, Th11;

    theorem :: CIRCLED1:14

    

     Th14: for V be RealLinearSpace holds ( Cir ( {} V)) = {}

    proof

      let V be RealLinearSpace;

      ( {} V) in ( Circled-Family ( {} V)) by Def2;

      hence thesis by SETFAM_1: 4;

    end;

    theorem :: CIRCLED1:15

    for V be RealLinearSpace, M be Subset of V, r be Real holds (r * ( Cir M)) = ( Cir (r * M))

    proof

      let V be RealLinearSpace, M be Subset of V, r be Real;

      thus (r * ( Cir M)) c= ( Cir (r * M))

      proof

        let x be object;

        per cases ;

          suppose

           A1: r = 0 ;

          per cases ;

            suppose M = {} ;

            then M = ( {} V);

            then ( Cir M) = {} by Th14;

            hence thesis by CONVEX1: 33;

          end;

            suppose

             A2: M <> {} ;

            then (r * M) = {( 0. V)} by A1, CONVEX1: 34;

            then

             A3: {( 0. V)} c= ( Cir (r * M)) by Th11;

            ( Cir M) <> {} by A2, Th11, XBOOLE_1: 3;

            then (r * ( Cir M)) = {( 0. V)} by A1, CONVEX1: 34;

            hence thesis by A3;

          end;

        end;

          suppose

           A4: r <> 0 ;

          

           A5: (r * ( Cir M)) = { (r * v) where v be Point of V : v in ( Cir M) } by CONVEX1:def 1;

          assume x in (r * ( Cir M));

          then

          consider v be Point of V such that

           A6: x = (r * v) and

           A7: v in ( Cir M) by A5;

          for W be set st W in ( Circled-Family (r * M)) holds (r * v) in W

          proof

            let W be set;

            assume

             A8: W in ( Circled-Family (r * M));

            then

            reconsider W as Subset of V;

            (r * M) c= W by A8, Def2;

            then ((r " ) * (r * M)) c= ((r " ) * W) by CONVEX1: 39;

            then (((r " ) * r) * M) c= ((r " ) * W) by CONVEX1: 37;

            then (1 * M) c= ((r " ) * W) by A4, XCMPLX_0:def 7;

            then

             A9: M c= ((r " ) * W) by CONVEX1: 32;

            W is circled by A8, Def2;

            then ((r " ) * W) is circled by Th2;

            then ((r " ) * W) in ( Circled-Family M) by A9, Def2;

            then ((r " ) * W) = { ((r " ) * w) where w be Point of V : w in W } & v in ((r " ) * W) by A7, CONVEX1:def 1, SETFAM_1:def 1;

            then

            consider w be Point of V such that

             A10: v = ((r " ) * w) and

             A11: w in W;

            (r * v) = ((r * (r " )) * w) by A10, RLVECT_1:def 7

            .= (1 * w) by A4, XCMPLX_0:def 7

            .= w by RLVECT_1:def 8;

            hence thesis by A11;

          end;

          hence thesis by A6, SETFAM_1:def 1;

        end;

      end;

      (r * M) c= (r * ( Cir M)) & (r * ( Cir M)) is circled by Th2, Th11, CONVEX1: 39;

      hence thesis by Th12;

    end;

    begin

    definition

      let V be RealLinearSpace, L be Linear_Combination of V;

      :: CIRCLED1:def4

      attr L is circled means

      : Def4: 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 :: CIRCLED1:16

    

     Th16: for V be RealLinearSpace, L be Linear_Combination of V st L is circled holds ( Carrier L) <> {}

    proof

      let V be RealLinearSpace, L be Linear_Combination of V;

      assume that

       A1: L is circled and

       A2: ( Carrier L) = {} ;

      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;

      consider f be FinSequence of REAL such that

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

      ( len F) = 0 by A2, A3, CARD_1: 27, FINSEQ_4: 62;

      then f = ( <*> the carrier of V) by A5;

      hence contradiction by A5, RVSUM_1: 72;

    end;

    theorem :: CIRCLED1:17

    

     Th17: for V be RealLinearSpace, L be Linear_Combination of V, v be VECTOR of V st L is circled & (L . v) <= 0 holds not v in ( Carrier L)

    proof

      let V be RealLinearSpace, L be Linear_Combination of V, v be VECTOR of V;

      assume that

       A1: L is circled and

       A2: (L . v) <= 0 ;

      per cases by A2;

        suppose (L . v) = 0 ;

        hence thesis by RLVECT_2: 19;

      end;

        suppose

         A3: (L . v) < 0 ;

        now

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

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

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

          assume v in ( Carrier L);

          then

          consider n be object such that

           A6: n in ( dom F) and

           A7: (F . n) = v by A4, FUNCT_1:def 3;

          reconsider n as Element of NAT by A6;

          consider f be FinSequence of REAL such that

           A8: ( len f) = ( len F) and ( Sum f) = 1 and

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

          n in ( Seg ( len F)) by A6, FINSEQ_1:def 3;

          then

           A10: n in ( dom f) by A8, FINSEQ_1:def 3;

          then (L . v) = (f . n) by A9, A7;

          hence contradiction by A3, A9, A10;

        end;

        hence thesis;

      end;

    end;

    theorem :: CIRCLED1:18

    for V be RealLinearSpace, L be Linear_Combination of V st L is circled holds L <> ( ZeroLC V) by Th16, RLVECT_2:def 5;

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

    registration

      let V be RealLinearSpace;

      cluster circled for Linear_Combination of V;

      existence

      proof

        set u = the Element of V;

        consider L be Linear_Combination of {u} such that

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

        take L;

        L is circled

        proof

          take <*u*>;

          

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

          proof

            reconsider f = <*jj*> as FinSequence of REAL ;

            take f;

            

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

            proof

              let n be Nat;

              assume n in ( dom f);

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

              then

               A4: n = 1 by TARSKI:def 1;

              

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

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

              hence thesis by A4, FINSEQ_1: 40;

            end;

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

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

            hence thesis by A3, FINSOP_1: 11;

          end;

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

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

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

          then ( Carrier L) = {u};

          hence thesis by A2, FINSEQ_1: 38, FINSEQ_3: 93;

        end;

        hence thesis;

      end;

    end

    definition

      let V be RealLinearSpace;

      mode circled_Combination of V is circled Linear_Combination of V;

    end

    registration

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

      cluster circled for Linear_Combination of M;

      existence

      proof

        consider u be object such that

         A1: u in M by XBOOLE_0:def 1;

        reconsider u as Element of V by A1;

        consider L be Linear_Combination of {u} such that

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

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

        then

        reconsider L as Linear_Combination of M by RLVECT_2: 21;

        take L;

        L is circled

        proof

          take <*u*>;

          

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

          proof

            reconsider f = <*jj*> as FinSequence of REAL ;

            take f;

            

             A4: for n be Nat st n in ( dom f) holds (f . n) = (L . ( <*u*> . n)) & (f . n) >= 0

            proof

              let n be Nat;

              assume n in ( dom f);

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

              then

               A5: n = 1 by TARSKI:def 1;

              then (f . n) = 1 by FINSEQ_1: 40;

              hence thesis by A2, A5, FINSEQ_1: 40;

            end;

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

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

            hence thesis by A4, FINSOP_1: 11;

          end;

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

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

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

          then ( Carrier L) = {u};

          hence thesis by A3, FINSEQ_1: 38, FINSEQ_3: 93;

        end;

        hence thesis;

      end;

    end

    definition

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

      mode circled_Combination of M is circled Linear_Combination of M;

    end

    definition

      let V be RealLinearSpace;

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

      :: CIRCLED1:def5

      func circledComb V -> set means for L be object holds L in it iff L is circled_Combination of V;

      existence

      proof

        consider A be set such that

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

        take A;

        let L be object;

        thus L in A implies L is circled_Combination of V by A1;

        assume L is circled_Combination of V;

        hence thesis by A1;

      end;

      uniqueness

      proof

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

      end;

    end

    definition

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

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

      :: CIRCLED1:def6

      func circledComb M -> set means for L be object holds L in it iff L is circled_Combination of M;

      existence

      proof

        consider A be set such that

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

        take A;

        let L be object;

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

        assume L is circled_Combination of M;

        hence thesis by A1;

      end;

      uniqueness

      proof

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

      end;

    end

    theorem :: CIRCLED1:19

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

    proof

      let V be RealLinearSpace, v be VECTOR of V;

      consider L be Linear_Combination of {v} such that

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

      consider F be FinSequence of the carrier of V such that

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

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

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

      then

       A3: {v} = ( Carrier L);

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

      then

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

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

      consider f be FinSequence such that

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

      

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

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

      then

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

      then f = <*jj*> by A1, A5, A6, A4, FINSEQ_1: 40;

      then

      reconsider f as FinSequence of REAL ;

      

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

      proof

        let n be Nat;

        assume

         A9: n in ( dom f);

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

        hence thesis by A1, A5, A6, A7, A4, A9, FINSEQ_1: 2, TARSKI:def 1;

      end;

      f = <*jj*> by A1, A5, A6, A7, A4, FINSEQ_1: 40;

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

      then

      reconsider L as circled_Combination of V by A2, A5, A8, Def4;

      

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

      take L;

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

      hence thesis by A10, RLVECT_1:def 8;

    end;

    theorem :: CIRCLED1:20

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

    proof

      let V be RealLinearSpace, v1,v2 be VECTOR of V;

      assume

       A1: v1 <> v2;

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

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

      consider F be FinSequence of the carrier of V such that

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

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

      consider f be FinSequence such that

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

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

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

      then

       A5: {v1, v2} = ( Carrier L);

      then

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

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

      then

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

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

      then

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

      now

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

          suppose F = <*v1, v2*>;

          then

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

          then f = <*jd, jd*> by A2, A4, A6, A8, A7, FINSEQ_1: 44;

          then f = ( <*(1 / 2)*> ^ <*(1 / 2)*>) by FINSEQ_1:def 9;

          

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

          .= {jd} by FINSEQ_1: 38;

          then

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

          

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

          proof

            let n be Nat;

            assume

             A11: n in ( dom f);

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

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

          end;

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

          

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

          .= 1;

          then

          reconsider L as circled_Combination of V by A3, A4, A10, Def4;

          take L;

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

          hence thesis;

        end;

          suppose F = <*v2, v1*>;

          then

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

          then f = <*jd, jd*> by A2, A4, A6, A8, A7, FINSEQ_1: 44;

          then f = ( <*(1 / 2)*> ^ <*(1 / 2)*>) by FINSEQ_1:def 9;

          

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

          .= {jd} by FINSEQ_1: 38;

          then

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

          

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

          proof

            let n be Nat;

            assume

             A14: n in ( dom f);

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

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

          end;

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

          

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

          .= 1;

          then

          reconsider L as circled_Combination of V by A3, A4, A13, Def4;

          take L;

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

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: CIRCLED1:21

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

    proof

      let V be RealLinearSpace, L1,L2 be circled_Combination of V, a,b be Real;

      assume (a * b) > 0 ;

      then

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

      then

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

      

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

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

      proof

        let x be object;

        assume

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

        per cases by A4, XBOOLE_0:def 3;

          suppose

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

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

          then

          consider v be Element of V such that

           A6: v = x and

           A7: ((a * L1) . v) <> 0 ;

          

           A8: (L1 . v) > 0 by A3, A5, A6, Th17;

          v in ( Carrier ((a * L1) + (b * L2)))

          proof

            per cases ;

              suppose

               A9: v in ( Carrier L2);

              then

               A10: (L2 . v) > 0 by Th17;

              per cases by A1;

                suppose

                 A11: a > 0 & b > 0 ;

                then (b * (L2 . v)) > 0 by A10, XREAL_1: 129;

                then ((b * L2) . v) > 0 by RLVECT_2:def 11;

                then

                 A12: (((a * L1) . v) + ((b * L2) . v)) > ((a * L1) . v) by XREAL_1: 29;

                (a * (L1 . v)) > 0 by A8, A11, XREAL_1: 129;

                then ((a * L1) . v) > 0 by RLVECT_2:def 11;

                then (((a * L1) + (b * L2)) . v) > 0 by A12, RLVECT_2:def 10;

                hence thesis by RLVECT_2: 19;

              end;

                suppose

                 A13: a < 0 & b < 0 ;

                then (a * (L1 . v)) < 0 by A3, A5, A6, Th17, XREAL_1: 132;

                then ((a * L1) . v) < 0 by RLVECT_2:def 11;

                then

                 A14: (((a * L1) . v) + ((b * L2) . v)) < ((b * L2) . v) by XREAL_1: 30;

                (b * (L2 . v)) < 0 by A9, A13, Th17, XREAL_1: 132;

                then ((b * L2) . v) < 0 by RLVECT_2:def 11;

                then (((a * L1) + (b * L2)) . v) < 0 by A14, RLVECT_2:def 10;

                hence thesis by RLVECT_2: 19;

              end;

            end;

              suppose not v in ( Carrier L2);

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

              then (b * (L2 . v)) = 0 ;

              then ((b * L2) . v) = 0 by RLVECT_2:def 11;

              then (((a * L1) . v) + ((b * L2) . v)) = ((a * L1) . v);

              then (((a * L1) + (b * L2)) . v) <> 0 by A7, RLVECT_2:def 10;

              hence thesis by RLVECT_2: 19;

            end;

          end;

          hence thesis by A6;

        end;

          suppose

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

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

          then

          consider v be Element of V such that

           A16: v = x and

           A17: ((b * L2) . v) <> 0 ;

          

           A18: (L2 . v) > 0 by A2, A15, A16, Th17;

          v in ( Carrier ((a * L1) + (b * L2)))

          proof

            per cases ;

              suppose

               A19: v in ( Carrier L1);

              then

               A20: (L1 . v) > 0 by Th17;

              per cases by A1;

                suppose

                 A21: a > 0 & b > 0 ;

                then (b * (L2 . v)) > 0 by A18, XREAL_1: 129;

                then ((b * L2) . v) > 0 by RLVECT_2:def 11;

                then

                 A22: (((a * L1) . v) + ((b * L2) . v)) > ((a * L1) . v) by XREAL_1: 29;

                (a * (L1 . v)) > 0 by A20, A21, XREAL_1: 129;

                then ((a * L1) . v) > 0 by RLVECT_2:def 11;

                then (((a * L1) + (b * L2)) . v) > 0 by A22, RLVECT_2:def 10;

                hence thesis by RLVECT_2: 19;

              end;

                suppose

                 A23: a < 0 & b < 0 ;

                then (a * (L1 . v)) < 0 by A19, Th17, XREAL_1: 132;

                then ((a * L1) . v) < 0 by RLVECT_2:def 11;

                then

                 A24: (((a * L1) . v) + ((b * L2) . v)) < ((b * L2) . v) by XREAL_1: 30;

                (b * (L2 . v)) < 0 by A2, A15, A16, A23, Th17, XREAL_1: 132;

                then ((b * L2) . v) < 0 by RLVECT_2:def 11;

                then (((a * L1) + (b * L2)) . v) < 0 by A24, RLVECT_2:def 10;

                hence thesis by RLVECT_2: 19;

              end;

            end;

              suppose not v in ( Carrier L1);

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

              then (a * (L1 . v)) = 0 ;

              then ((a * L1) . v) = 0 by RLVECT_2:def 11;

              then (((a * L1) . v) + ((b * L2) . v)) = ((b * L2) . v);

              then (((a * L1) + (b * L2)) . v) <> 0 by A17, RLVECT_2:def 10;

              hence thesis by RLVECT_2: 19;

            end;

          end;

          hence thesis by A16;

        end;

      end;

      then

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

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

      hence thesis by A25;

    end;

    theorem :: CIRCLED1:22

    

     Th22: for V be RealLinearSpace, v be VECTOR of V, L be Linear_Combination of V st L is circled & ( Carrier L) = {v} holds (L . v) = 1 & ( Sum L) = ((L . v) * v)

    proof

      let V be RealLinearSpace, v be VECTOR of V, L be Linear_Combination of V;

      assume that

       A1: L is circled and

       A2: ( Carrier L) = {v};

      reconsider L as Linear_Combination of {v} by A2, RLVECT_2:def 6;

      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) by FINSEQ_1: 2, TARSKI:def 1;

      then

       A11: (f . 1) = (f /. 1) by PARTFUN1:def 6;

      then f = <*r*> by A9, FINSEQ_1:def 8;

      then

       A12: ( Sum f) = r by FINSOP_1: 11;

      (f . 1) = (L . (F . 1)) by A8, A10;

      hence thesis by A7, A11, A12, A5, FINSEQ_1:def 8, RLVECT_2: 32;

    end;

    theorem :: CIRCLED1:23

    

     Th23: for V be RealLinearSpace, v1,v2 be VECTOR of V, L be Linear_Combination of V st L is circled & ( Carrier L) = {v1, v2} & v1 <> v2 holds ((L . v1) + (L . v2)) = 1 & (L . v1) >= 0 & (L . v2) >= 0 & ( Sum L) = (((L . v1) * v1) + ((L . v2) * v2))

    proof

      let V be RealLinearSpace, v1,v2 be VECTOR of V, L be Linear_Combination of V;

      assume that

       A1: L is circled and

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

       A3: v1 <> v2;

      reconsider L as Linear_Combination of {v1, v2} by A2, RLVECT_2:def 6;

      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: 1 in ( dom f) by TARSKI:def 2;

      then

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

      then (f /. 1) = (L . (F . 1)) by A11, PARTFUN1:def 6;

      then

      reconsider r1 = (L . (F . 1)) as Element of REAL ;

      

       A13: 2 in ( dom f) by A10, TARSKI:def 2;

      then

       A14: (f . 2) = (L . (F . 2)) by A8;

      then (f /. 2) = (L . (F . 2)) by A13, PARTFUN1:def 6;

      then

      reconsider r2 = (L . (F . 2)) as Element of REAL ;

      

       A15: f = <*r1, r2*> by A9, A12, A14, FINSEQ_1: 44;

      now

        per cases by A2, A3, A4, FINSEQ_3: 99;

          suppose F = <*v1, v2*>;

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

          hence ((L . v1) + (L . v2)) = 1 & (L . v1) >= 0 & (L . v2) >= 0 by A7, A8, A11, A13, A12, A14, A15, RVSUM_1: 77;

        end;

          suppose F = <*v2, v1*>;

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

          hence ((L . v1) + (L . v2)) = 1 & (L . v1) >= 0 & (L . v2) >= 0 by A7, A8, A11, A13, A12, A14, A15, RVSUM_1: 77;

        end;

      end;

      hence thesis by A3, RLVECT_2: 33;

    end;

    theorem :: CIRCLED1:24

    for V be RealLinearSpace, v be VECTOR of V, L be Linear_Combination of {v} st L is circled holds (L . v) = 1 & ( Sum L) = ((L . v) * v)

    proof

      let V be RealLinearSpace, v be VECTOR of V, L be Linear_Combination of {v};

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

      then

       A1: ( Carrier L) = {} or ( Carrier L) = {v} by ZFMISC_1: 33;

      assume L is circled;

      hence thesis by A1, Th16, Th22;

    end;

    theorem :: CIRCLED1:25

    for V be RealLinearSpace, v1,v2 be VECTOR of V, L be Linear_Combination of {v1, v2} st v1 <> v2 & L is circled holds ((L . v1) + (L . v2)) = 1 & (L . v1) >= 0 & (L . v2) >= 0 & ( Sum L) = (((L . v1) * v1) + ((L . v2) * v2))

    proof

      let V be RealLinearSpace, v1,v2 be VECTOR of V, L be Linear_Combination of {v1, v2};

      assume that

       A1: v1 <> v2 and

       A2: L is circled;

      

       A3: ( Carrier L) c= {v1, v2} & ( Carrier L) <> {} by A2, Th16, RLVECT_2:def 6;

      now

        per cases by A3, ZFMISC_1: 36;

          suppose

           A4: ( Carrier L) = {v1};

          then not v2 in ( Carrier L) by A1, TARSKI:def 1;

          then not v2 in { v where v be Element of V : (L . v) <> 0 } by RLVECT_2:def 4;

          then (L . v2) = 0 ;

          hence ((L . v1) + (L . v2)) = 1 & (L . v1) >= 0 & (L . v2) >= 0 by A2, A4, Th22;

        end;

          suppose

           A5: ( Carrier L) = {v2};

          then not v1 in ( Carrier L) by A1, TARSKI:def 1;

          then not v1 in { v where v be Element of V : (L . v) <> 0 } by RLVECT_2:def 4;

          then (L . v1) = 0 ;

          hence ((L . v1) + (L . v2)) = 1 & (L . v1) >= 0 & (L . v2) >= 0 by A2, A5, Th22;

        end;

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

          hence ((L . v1) + (L . v2)) = 1 & (L . v1) >= 0 & (L . v2) >= 0 by A1, A2, Th23;

        end;

      end;

      hence thesis by A1, RLVECT_2: 33;

    end;