mathmorp.miz



    begin

    definition

      let T be non empty addMagma, p be Element of T, X be Subset of T;

      :: MATHMORP:def1

      func X + p -> Subset of T equals { (q + p) where q be Element of T : q in X };

      coherence

      proof

        now

          let x be object;

          assume x in { (q + p) where q be Point of T : q in X };

          then ex q be Point of T st x = (q + p) & q in X;

          hence x in the carrier of T;

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    definition

      let T be non empty addLoopStr, X be Subset of T;

      :: MATHMORP:def2

      func X ! -> Subset of T equals { ( - q) where q be Point of T : q in X };

      coherence

      proof

        now

          let x be object;

          assume x in { ( - q) where q be Point of T : q in X };

          then ex q be Point of T st x = ( - q) & q in X;

          hence x in the carrier of T;

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    definition

      let T be non empty addMagma, X,B be Subset of T;

      :: MATHMORP:def3

      func X (-) B -> Subset of T equals { y where y be Point of T : (B + y) c= X };

      coherence

      proof

        now

          let x be object;

          assume x in { y where y be Point of T : (B + y) c= X };

          then ex q be Point of T st x = q & (B + q) c= X;

          hence x in the carrier of T;

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    notation

      let T be non empty addLoopStr;

      let A,B be Subset of T;

      synonym A (+) B for A + B;

    end

    reserve T for non empty Abelian add-associative right_zeroed right_complementable RLSStruct,

X,Y,Z,B,C,B1,B2 for Subset of T,

x,y,p for Point of T;

    theorem :: MATHMORP:1

    

     Th1: for T be add-associative right_zeroed right_complementable non empty RLSStruct, B be Subset of T holds ((B ! ) ! ) = B

    proof

      let T be add-associative right_zeroed right_complementable non empty RLSStruct, B be Subset of T;

      thus ((B ! ) ! ) c= B

      proof

        let x be object;

        assume x in ((B ! ) ! );

        then

        consider q be Element of T such that

         A1: x = ( - q) and

         A2: q in (B ! );

        ex q1 be Element of T st q = ( - q1) & q1 in B by A2;

        hence thesis by A1;

      end;

      let x be object;

      assume

       A3: x in B;

      then

      reconsider xx = x as Point of T;

      ( - xx) in { ( - q) where q be Point of T : q in B } by A3;

      then ( - ( - xx)) in { ( - q) where q be Point of T : q in (B ! ) };

      hence thesis;

    end;

    theorem :: MATHMORP:2

    

     Th2: ( {( 0. T)} + x) = {x}

    proof

      thus ( {( 0. T)} + x) c= {x}

      proof

        let a be object;

        assume a in ( {( 0. T)} + x);

        then

        consider q be Point of T such that

         A1: a = (q + x) and

         A2: q in {( 0. T)};

         {q} c= {( 0. T)} by A2, ZFMISC_1: 31;

        then q = ( 0. T) by ZFMISC_1: 18;

        then {a} c= {x} by A1;

        hence thesis by ZFMISC_1: 31;

      end;

      let a be object;

      assume a in {x};

      then {a} c= {x} by ZFMISC_1: 31;

      then a = x by ZFMISC_1: 18;

      then

       A3: a = (( 0. T) + x);

      ( 0. T) in {( 0. T)} by ZFMISC_1: 31;

      hence thesis by A3;

    end;

    theorem :: MATHMORP:3

    

     Th3: B1 c= B2 implies (B1 + p) c= (B2 + p)

    proof

      assume

       A1: B1 c= B2;

      let p1 be object;

      assume p1 in (B1 + p);

      then ex p2 be Point of T st p1 = (p2 + p) & p2 in B1;

      hence thesis by A1;

    end;

    theorem :: MATHMORP:4

    

     Th4: for X st X = {} holds (X + x) = {}

    proof

      let X;

      assume

       A1: X = {} ;

      now

        given y be object such that

         A2: y in (X + x);

        ex y1 be Point of T st y = (y1 + x) & y1 in X by A2;

        hence contradiction by A1;

      end;

      hence thesis by XBOOLE_0:def 1;

    end;

    theorem :: MATHMORP:5

    (X (-) {( 0. T)}) = X

    proof

      thus (X (-) {( 0. T)}) c= X

      proof

        let x be object;

        assume x in (X (-) {( 0. T)});

        then ex y be Point of T st x = y & ( {( 0. T)} + y) c= X;

        then {x} c= X by Th2;

        hence thesis by ZFMISC_1: 31;

      end;

      let x be object;

      assume

       A1: x in X;

      then

      reconsider xx = x as Point of T;

       {x} c= X by A1, ZFMISC_1: 31;

      then ( {( 0. T)} + xx) c= X by Th2;

      hence thesis;

    end;

    

     Lm1: ( {x} + y) = ( {y} + x)

    proof

      thus ( {x} + y) c= ( {y} + x)

      proof

        let x1 be object;

        assume x1 in ( {x} + y);

        then

        consider p1 be Point of T such that

         A1: x1 = (p1 + y) and

         A2: p1 in {x};

         {p1} c= {x} by A2, ZFMISC_1: 31;

        then

         A3: x1 = (x + y) by A1, ZFMISC_1: 18;

        y in {y} by TARSKI:def 1;

        hence thesis by A3;

      end;

      let x1 be object;

      assume x1 in ( {y} + x);

      then

      consider p1 be Point of T such that

       A4: x1 = (p1 + x) and

       A5: p1 in {y};

       {p1} c= {y} by A5, ZFMISC_1: 31;

      then

       A6: x1 = (x + y) by A4, ZFMISC_1: 18;

      x in {x} by TARSKI:def 1;

      hence thesis by A6;

    end;

    theorem :: MATHMORP:6

    (X (+) {( 0. T)}) = X

    proof

      thus (X (+) {( 0. T)}) c= X

      proof

        let x be object;

        assume x in (X (+) {( 0. T)});

        then

        consider y,z be Point of T such that

         A1: x = (y + z) & y in X and

         A2: z in {( 0. T)};

         {z} c= {( 0. T)} by A2, ZFMISC_1: 31;

        then z = ( 0. T) by ZFMISC_1: 18;

        hence thesis by A1;

      end;

      let x be object;

      assume

       A3: x in X;

      then

      reconsider x as Point of T;

      ( 0. T) in {( 0. T)} by TARSKI:def 1;

      then (x + ( 0. T)) in { (y + z) where y,z be Point of T : y in X & z in {( 0. T)} } by A3;

      hence thesis;

    end;

    theorem :: MATHMORP:7

    (X (+) {x}) = (X + x)

    proof

      thus (X (+) {x}) c= (X + x)

      proof

        let p be object;

        assume p in (X (+) {x});

        then

        consider y,z be Point of T such that

         A1: p = (y + z) and

         A2: y in X and

         A3: z in {x};

         {z} c= {x} by A3, ZFMISC_1: 31;

        then p = (y + x) by A1, ZFMISC_1: 18;

        hence thesis by A2;

      end;

      let p be object;

      assume p in (X + x);

      then

       A4: ex q be Point of T st p = (q + x) & q in X;

      x in {x} by TARSKI:def 1;

      hence thesis by A4;

    end;

    theorem :: MATHMORP:8

    

     Th8: for X, Y st Y = {} holds (X (-) Y) = the carrier of T

    proof

      let X, Y;

      assume

       A1: Y = {} ;

      { y where y be Point of T : (Y + y) c= X } = the carrier of T

      proof

        thus { y where y be Point of T : (Y + y) c= X } c= the carrier of T

        proof

          let x be object;

          assume x in { y where y be Point of T : (Y + y) c= X };

          then ex y be Point of T st x = y & (Y + y) c= X;

          hence thesis;

        end;

        let x be object;

        assume x in the carrier of T;

        then

        reconsider a = x as Point of T;

        (Y + a) = {} by A1, Th4;

        then (Y + a) c= X;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: MATHMORP:9

    

     Th9: X c= Y implies (X (-) B) c= (Y (-) B) & (X (+) B) c= (Y (+) B)

    proof

      assume

       A1: X c= Y;

      thus (X (-) B) c= (Y (-) B)

      proof

        let p be object;

        assume p in (X (-) B);

        then

        consider p1 be Point of T such that

         A2: p = p1 and

         A3: (B + p1) c= X;

        (B + p1) c= Y by A1, A3;

        hence thesis by A2;

      end;

      let p be object;

      assume p in (X (+) B);

      then ex p1,p2 be Point of T st p = (p1 + p2) & p1 in X & p2 in B;

      hence thesis by A1;

    end;

    theorem :: MATHMORP:10

    

     Th10: B1 c= B2 implies (X (-) B2) c= (X (-) B1) & (X (+) B1) c= (X (+) B2)

    proof

      assume

       A1: B1 c= B2;

      thus (X (-) B2) c= (X (-) B1)

      proof

        let p be object;

        assume p in (X (-) B2);

        then

        consider p1 be Point of T such that

         A2: p = p1 and

         A3: (B2 + p1) c= X;

        (B1 + p1) c= (B2 + p1) by A1, Th3;

        then (B1 + p1) c= X by A3;

        hence thesis by A2;

      end;

      let p be object;

      assume p in (X (+) B1);

      then ex x,b be Point of T st p = (x + b) & x in X & b in B1;

      hence thesis by A1;

    end;

    theorem :: MATHMORP:11

    ( 0. T) in B implies (X (-) B) c= X & X c= (X (+) B)

    proof

      assume

       A1: ( 0. T) in B;

      thus (X (-) B) c= X

      proof

        let p be object;

        assume p in (X (-) B);

        then

        consider p1 be Point of T such that

         A2: p = p1 and

         A3: (B + p1) c= X;

        (( 0. T) + p1) in { (q + p1) where q be Point of T : q in B } by A1;

        then (( 0. T) + p1) in X by A3;

        hence thesis by A2;

      end;

      let p be object;

      assume

       A4: p in X;

      then

      reconsider p as Point of T;

      (p + ( 0. T)) in { (x + b) where x,b be Point of T : x in X & b in B } by A1, A4;

      hence thesis;

    end;

    theorem :: MATHMORP:12

    

     Th12: (X (+) Y) = (Y (+) X)

    proof

      thus (X (+) Y) c= (Y (+) X)

      proof

        let p be object;

        assume p in (X (+) Y);

        then ex p1,p2 be Point of T st p = (p1 + p2) & p1 in X & p2 in Y;

        hence thesis;

      end;

      let p be object;

      assume p in (Y (+) X);

      then ex p1,p2 be Point of T st p = (p1 + p2) & p1 in Y & p2 in X;

      hence thesis;

    end;

    

     Lm2: ((p - x) + x) = p & ((p + x) - x) = p

    proof

      ((p + x) - x) = (p + (x - x)) by RLVECT_1:def 3

      .= (p + ( 0. T)) by RLVECT_1: 15

      .= p;

      hence thesis by RLVECT_1: 28;

    end;

    theorem :: MATHMORP:13

    

     Th13: (Y + y) c= (X + x) iff (Y + (y - x)) c= X

    proof

      thus (Y + y) c= (X + x) implies (Y + (y - x)) c= X

      proof

        assume

         A1: (Y + y) c= (X + x);

        let p be object;

        assume p in (Y + (y - x));

        then

        consider q1 be Point of T such that

         A2: p = (q1 + (y - x)) and

         A3: q1 in Y;

        reconsider p as Point of T by A2;

        p = ((q1 + y) - x) by A2, RLVECT_1: 28;

        then

         A4: (p + x) = (q1 + y) by Lm2;

        (q1 + y) in { (q + y) where q be Point of T : q in Y } by A3;

        then (p + x) in (X + x) by A1, A4;

        then

        consider p1 be Point of T such that

         A5: (p + x) = (p1 + x) and

         A6: p1 in X;

        ((p + x) - x) = p1 by A5, Lm2;

        hence thesis by A6, Lm2;

      end;

      assume

       A7: (Y + (y - x)) c= X;

      let p be object;

      assume p in (Y + y);

      then

      consider q1 be Point of T such that

       A8: p = (q1 + y) and

       A9: q1 in Y;

      reconsider p as Point of T by A8;

      (p - x) = (q1 + (y - x)) & (q1 + (y - x)) in { (q + (y - x)) where q be Point of T : q in Y } by A8, A9, RLVECT_1: 28;

      then ((p - x) + x) in { (q + x) where q be Point of T : q in X } by A7;

      hence thesis by Lm2;

    end;

    theorem :: MATHMORP:14

    

     Th14: ((X + p) (-) Y) = ((X (-) Y) + p)

    proof

      thus ((X + p) (-) Y) c= ((X (-) Y) + p)

      proof

        let x be object;

        assume x in ((X + p) (-) Y);

        then

        consider y be Point of T such that

         A1: x = y and

         A2: (Y + y) c= (X + p);

        (Y + (y - p)) c= X by A2, Th13;

        then (y - p) in { y1 where y1 be Point of T : (Y + y1) c= X };

        then ((y - p) + p) in { (q + p) where q be Point of T : q in (X (-) Y) };

        hence thesis by A1, Lm2;

      end;

      let x be object;

      assume x in ((X (-) Y) + p);

      then

      consider y be Point of T such that

       A3: x = (y + p) and

       A4: y in (X (-) Y);

      reconsider x as Point of T by A3;

      (x - p) = y & ex y2 be Point of T st y = y2 & (Y + y2) c= X by A3, A4, Lm2;

      then (Y + x) c= (X + p) by Th13;

      hence thesis;

    end;

    theorem :: MATHMORP:15

    

     Th15: ((X + p) (+) Y) = ((X (+) Y) + p)

    proof

      thus ((X + p) (+) Y) c= ((X (+) Y) + p)

      proof

        let x be object;

        assume x in ((X + p) (+) Y);

        then

        consider x2,y2 be Point of T such that

         A1: x = (x2 + y2) and

         A2: x2 in (X + p) and

         A3: y2 in Y;

        consider x3 be Point of T such that

         A4: x2 = (x3 + p) & x3 in X by A2;

        x = ((x3 + y2) + p) & (x3 + y2) in (X (+) Y) by A1, A3, A4, RLVECT_1:def 3;

        hence thesis;

      end;

      let x be object;

      assume x in ((X (+) Y) + p);

      then

      consider x2 be Point of T such that

       A5: x = (x2 + p) and

       A6: x2 in (X (+) Y);

      consider x3,y3 be Point of T such that

       A7: x2 = (x3 + y3) and

       A8: x3 in X and

       A9: y3 in Y by A6;

      

       A10: (x3 + p) in (X + p) by A8;

      x = ((x3 + p) + y3) by A5, A7, RLVECT_1:def 3;

      hence thesis by A9, A10;

    end;

    theorem :: MATHMORP:16

    

     Th16: ((X + x) + y) = (X + (x + y))

    proof

      thus ((X + x) + y) c= (X + (x + y))

      proof

        let p be object;

        assume p in ((X + x) + y);

        then

        consider x2 be Point of T such that

         A1: p = (x2 + y) and

         A2: x2 in (X + x);

        consider x3 be Point of T such that

         A3: x2 = (x3 + x) and

         A4: x3 in X by A2;

        p = (x3 + (x + y)) by A1, A3, RLVECT_1:def 3;

        hence thesis by A4;

      end;

      let p be object;

      assume p in (X + (x + y));

      then

      consider x2 be Point of T such that

       A5: p = (x2 + (x + y)) & x2 in X;

      p = ((x2 + x) + y) & (x2 + x) in (X + x) by A5, RLVECT_1:def 3;

      hence thesis;

    end;

    theorem :: MATHMORP:17

    

     Th17: (X (-) (Y + p)) = ((X (-) Y) + ( - p))

    proof

      thus (X (-) (Y + p)) c= ((X (-) Y) + ( - p))

      proof

        let x be object;

        assume x in (X (-) (Y + p));

        then

        consider y be Point of T such that

         A1: x = y and

         A2: ((Y + p) + y) c= X;

        (Y + (y + p)) c= X by A2, Th16;

        then (y + p) in { y1 where y1 be Point of T : (Y + y1) c= X };

        then ((y + p) - p) in ((X (-) Y) + ( - p));

        hence thesis by A1, Lm2;

      end;

      let x be object;

      assume x in ((X (-) Y) + ( - p));

      then

      consider y be Point of T such that

       A3: x = (y + ( - p)) and

       A4: y in (X (-) Y);

      reconsider x as Point of T by A3;

      (x + p) = ((y - p) + p) by A3;

      then

       A5: (x + p) = y by Lm2;

      ex y2 be Point of T st y = y2 & (Y + y2) c= X by A4;

      then ((Y + p) + x) c= X by A5, Th16;

      hence thesis;

    end;

    theorem :: MATHMORP:18

    (X (+) (Y + p)) = ((X (+) Y) + p)

    proof

      thus (X (+) (Y + p)) c= ((X (+) Y) + p)

      proof

        let x be object;

        assume x in (X (+) (Y + p));

        then

        consider x2,y2 be Point of T such that

         A1: x = (x2 + y2) & x2 in X and

         A2: y2 in (Y + p);

        consider y3 be Point of T such that

         A3: y2 = (y3 + p) & y3 in Y by A2;

        x = ((x2 + y3) + p) & (x2 + y3) in (X (+) Y) by A1, A3, RLVECT_1:def 3;

        hence thesis;

      end;

      let x be object;

      assume x in ((X (+) Y) + p);

      then

      consider x2 be Point of T such that

       A4: x = (x2 + p) and

       A5: x2 in (X (+) Y);

      consider x3,y3 be Point of T such that

       A6: x2 = (x3 + y3) and

       A7: x3 in X and

       A8: y3 in Y by A5;

      

       A9: (y3 + p) in (Y + p) by A8;

      x = (x3 + (y3 + p)) by A4, A6, RLVECT_1:def 3;

      hence thesis by A7, A9;

    end;

    theorem :: MATHMORP:19

    

     Th19: x in X implies (B + x) c= (B (+) X)

    proof

      assume

       A1: x in X;

      let y be object;

      assume y in (B + x);

      then ex y1 be Point of T st y = (y1 + x) & y1 in B;

      hence thesis by A1;

    end;

    theorem :: MATHMORP:20

    

     Th20: X c= ((X (+) B) (-) B)

    proof

      let x be object;

      assume

       A1: x in X;

      then

      consider x1 be Point of T such that

       A2: x1 = x;

      (B + x1) c= (B (+) X) by A1, A2, Th19;

      then x in ((B (+) X) (-) B) by A2;

      hence thesis by Th12;

    end;

    theorem :: MATHMORP:21

    

     Th21: (X + ( 0. T)) = X

    proof

      thus (X + ( 0. T)) c= X

      proof

        let x be object;

        assume x in (X + ( 0. T));

        then ex q be Point of T st x = (q + ( 0. T)) & q in X;

        hence thesis;

      end;

      let x be object;

      assume

       A1: x in X;

      then

      reconsider x1 = x as Point of T;

      x1 = (x1 + ( 0. T));

      hence thesis by A1;

    end;

    theorem :: MATHMORP:22

    (X (-) {x}) = (X + ( - x))

    proof

      thus (X (-) {x}) c= (X + ( - x))

      proof

        let y be object;

        assume y in (X (-) {x});

        then

        consider p be Point of T such that

         A1: p = y and

         A2: ( {x} + p) c= X;

        ( {p} + x) c= X by A2, Lm1;

        then (( {p} + x) + ( - x)) c= (X + ( - x)) by Th3;

        then ( {p} + (x + ( - x))) c= (X + ( - x)) by Th16;

        then ( {p} + ( 0. T)) c= (X + ( - x)) by RLVECT_1: 5;

        then {p} c= (X + ( - x)) by Th21;

        hence thesis by A1, ZFMISC_1: 31;

      end;

      let y be object;

      assume y in (X + ( - x));

      then

      consider p be Point of T such that

       A3: y = (p + ( - x)) and

       A4: p in X;

      reconsider y as Point of T by A3;

      y = (p - x) by A3;

      then

       A5: (y + x) = p by Lm2;

      ( {x} + y) c= X

      proof

        let q be object;

        assume q in ( {x} + y);

        then

        consider qq be Point of T such that

         A6: q = (qq + y) and

         A7: qq in {x};

         {qq} c= {x} by A7, ZFMISC_1: 31;

        hence thesis by A4, A5, A6, ZFMISC_1: 18;

      end;

      hence thesis;

    end;

    

     Lm3: ((X (-) B) (+) B) c= X

    proof

      let x be object;

      assume x in ((X (-) B) (+) B);

      then

      consider y1,y2 be Point of T such that

       A1: x = (y1 + y2) and

       A2: y1 in (X (-) B) and

       A3: y2 in B;

      consider y be Point of T such that

       A4: y1 = y and

       A5: (B + y) c= X by A2;

      x in (B + y) by A1, A3, A4;

      hence thesis by A5;

    end;

    theorem :: MATHMORP:23

    

     Th23: (X (-) (Y (+) Z)) = ((X (-) Y) (-) Z)

    proof

      

       A1: ((X (-) Y) (+) Y) c= X by Lm3;

      thus (X (-) (Y (+) Z)) c= ((X (-) Y) (-) Z)

      proof

        let p be object;

        assume p in (X (-) (Y (+) Z));

        then

        consider x be Point of T such that

         A2: p = x and

         A3: ((Y (+) Z) + x) c= X;

        ((Y + x) (+) Z) c= X by A3, Th15;

        then (Z (+) (Y + x)) c= X by Th12;

        then

         A4: ((Z (+) (Y + x)) (-) (Y + x)) c= (X (-) (Y + x)) by Th9;

        Z c= ((Z (+) (Y + x)) (-) (Y + x)) by Th20;

        then Z c= (X (-) (Y + x)) by A4;

        then Z c= ((X (-) Y) + ( - x)) by Th17;

        then (Z + x) c= (((X (-) Y) + ( - x)) + x) by Th3;

        then (Z + x) c= ((X (-) Y) + (( - x) + x)) by Th16;

        then (Z + x) c= ((X (-) Y) + (x - x));

        then (Z + x) c= ((X (-) Y) + ( 0. T)) by RLVECT_1: 15;

        then (Z + x) c= (X (-) Y) by Th21;

        hence thesis by A2;

      end;

      let p be object;

      assume p in ((X (-) Y) (-) Z);

      then

      consider y be Point of T such that

       A5: p = y and

       A6: (Z + y) c= (X (-) Y);

      ((Z + y) (+) Y) c= ((X (-) Y) (+) Y) by A6, Th9;

      then ((Z + y) (+) Y) c= X by A1;

      then ((Z (+) Y) + y) c= X by Th15;

      then p in (X (-) (Z (+) Y)) by A5;

      hence thesis by Th12;

    end;

    theorem :: MATHMORP:24

    (X (-) (Y (+) Z)) = ((X (-) Z) (-) Y)

    proof

      (X (-) (Y (+) Z)) = (X (-) (Z (+) Y)) by Th12

      .= ((X (-) Z) (-) Y) by Th23;

      hence thesis;

    end;

    theorem :: MATHMORP:25

    (X (+) (Y (-) Z)) c= ((X (+) Y) (-) Z)

    proof

      let x be object;

      assume x in (X (+) (Y (-) Z));

      then

      consider a,b be Point of T such that

       A1: x = (a + b) and

       A2: a in X and

       A3: b in (Y (-) Z);

      ex c be Point of T st b = c & (Z + c) c= Y by A3;

      then ((Z + b) + a) c= (Y + a) by Th3;

      then

       A4: (Z + (b + a)) c= (Y + a) by Th16;

      (Y + a) c= (Y (+) X) by A2, Th19;

      then (Z + (b + a)) c= (Y (+) X) by A4;

      then x in ((Y (+) X) (-) Z) by A1;

      hence thesis by Th12;

    end;

    theorem :: MATHMORP:26

    (X (+) (Y (+) Z)) = ((X (+) Y) (+) Z)

    proof

      thus (X (+) (Y (+) Z)) c= ((X (+) Y) (+) Z)

      proof

        let p be object;

        assume p in (X (+) (Y (+) Z));

        then

        consider x1,p2 be Point of T such that

         A1: p = (x1 + p2) & x1 in X and

         A2: p2 in (Y (+) Z);

        consider y,z be Point of T such that

         A3: p2 = (y + z) & y in Y and

         A4: z in Z by A2;

        set p3 = (x1 + y);

        p = ((x1 + y) + z) & p3 in (X (+) Y) by A1, A3, RLVECT_1:def 3;

        hence thesis by A4;

      end;

      let p be object;

      assume p in ((X (+) Y) (+) Z);

      then

      consider x1,p2 be Point of T such that

       A5: p = (x1 + p2) and

       A6: x1 in (X (+) Y) and

       A7: p2 in Z;

      consider y,z be Point of T such that

       A8: x1 = (y + z) and

       A9: y in X and

       A10: z in Y by A6;

      set p3 = (z + p2);

      p = (y + (z + p2)) & p3 in (Y (+) Z) by A5, A7, A8, A10, RLVECT_1:def 3;

      hence thesis by A9;

    end;

    theorem :: MATHMORP:27

    

     Th27: ((B \/ C) + y) = ((B + y) \/ (C + y))

    proof

      thus ((B \/ C) + y) c= ((B + y) \/ (C + y))

      proof

        let x be object;

        assume x in ((B \/ C) + y);

        then

        consider y2 be Point of T such that

         A1: x = (y2 + y) and

         A2: y2 in (B \/ C);

        y2 in B or y2 in C by A2, XBOOLE_0:def 3;

        then x in { (y1 + y) where y1 be Point of T : y1 in B } or x in { (y1 + y) where y1 be Point of T : y1 in C } by A1;

        hence thesis by XBOOLE_0:def 3;

      end;

      let x be object;

      assume x in ((B + y) \/ (C + y));

      then x in (B + y) or x in (C + y) by XBOOLE_0:def 3;

      then

      consider y2 be Point of T such that

       A3: x = (y2 + y) & y2 in B or x = (y2 + y) & y2 in C;

      y2 in (B \/ C) by A3, XBOOLE_0:def 3;

      hence thesis by A3;

    end;

    theorem :: MATHMORP:28

    

     Th28: ((B /\ C) + y) = ((B + y) /\ (C + y))

    proof

      thus ((B /\ C) + y) c= ((B + y) /\ (C + y))

      proof

        let x be object;

        assume x in ((B /\ C) + y);

        then

        consider y2 be Point of T such that

         A1: x = (y2 + y) and

         A2: y2 in (B /\ C);

        y2 in C by A2, XBOOLE_0:def 4;

        then

         A3: x in { (y1 + y) where y1 be Point of T : y1 in C } by A1;

        y2 in B by A2, XBOOLE_0:def 4;

        then x in { (y1 + y) where y1 be Point of T : y1 in B } by A1;

        hence thesis by A3, XBOOLE_0:def 4;

      end;

      let x be object;

      assume

       A4: x in ((B + y) /\ (C + y));

      then x in (B + y) by XBOOLE_0:def 4;

      then

      consider y3 be Point of T such that

       A5: x = (y3 + y) and

       A6: y3 in B;

      x in (C + y) by A4, XBOOLE_0:def 4;

      then

      consider y2 be Point of T such that

       A7: x = (y2 + y) and

       A8: y2 in C;

      ((y2 + y) - y) = y3 by A5, A7, Lm2;

      then

       A9: y2 = y3 by Lm2;

      then y2 in (B /\ C) by A6, A8, XBOOLE_0:def 4;

      hence thesis by A5, A9;

    end;

    theorem :: MATHMORP:29

    (X (-) (B \/ C)) = ((X (-) B) /\ (X (-) C))

    proof

      thus (X (-) (B \/ C)) c= ((X (-) B) /\ (X (-) C))

      proof

        let x be object;

        assume x in (X (-) (B \/ C));

        then

        consider y be Point of T such that

         A1: x = y and

         A2: ((B \/ C) + y) c= X;

        

         A3: ((B + y) \/ (C + y)) c= X by A2, Th27;

        then (C + y) c= X by XBOOLE_1: 11;

        then

         A4: x in { y1 where y1 be Point of T : (C + y1) c= X } by A1;

        (B + y) c= X by A3, XBOOLE_1: 11;

        then x in { y1 where y1 be Point of T : (B + y1) c= X } by A1;

        hence thesis by A4, XBOOLE_0:def 4;

      end;

      let x be object;

      assume

       A5: x in ((X (-) B) /\ (X (-) C));

      then x in (X (-) B) by XBOOLE_0:def 4;

      then

      consider y be Point of T such that

       A6: x = y and

       A7: (B + y) c= X;

      x in (X (-) C) by A5, XBOOLE_0:def 4;

      then ex y2 be Point of T st x = y2 & (C + y2) c= X;

      then ((B + y) \/ (C + y)) c= X by A6, A7, XBOOLE_1: 8;

      then ((B \/ C) + y) c= X by Th27;

      hence thesis by A6;

    end;

    theorem :: MATHMORP:30

    (X (+) (B \/ C)) = ((X (+) B) \/ (X (+) C))

    proof

      thus (X (+) (B \/ C)) c= ((X (+) B) \/ (X (+) C))

      proof

        let x be object;

        assume x in (X (+) (B \/ C));

        then

        consider y3,y4 be Point of T such that

         A1: x = (y3 + y4) & y3 in X and

         A2: y4 in (B \/ C);

        y4 in B or y4 in C by A2, XBOOLE_0:def 3;

        then x in { (y1 + y2) where y1,y2 be Point of T : y1 in X & y2 in B } or x in { (y1 + y2) where y1,y2 be Point of T : y1 in X & y2 in C } by A1;

        hence thesis by XBOOLE_0:def 3;

      end;

      let x be object;

      assume x in ((X (+) B) \/ (X (+) C));

      then x in (X (+) B) or x in (X (+) C) by XBOOLE_0:def 3;

      then

      consider y3,y4 be Point of T such that

       A3: x = (y3 + y4) & y3 in X & y4 in B or x = (y3 + y4) & y3 in X & y4 in C;

      y4 in (B \/ C) by A3, XBOOLE_0:def 3;

      hence thesis by A3;

    end;

    theorem :: MATHMORP:31

    ((X (-) B) \/ (Y (-) B)) c= ((X \/ Y) (-) B)

    proof

      let x be object;

      assume x in ((X (-) B) \/ (Y (-) B));

      then x in (X (-) B) or x in (Y (-) B) by XBOOLE_0:def 3;

      then

      consider y be Point of T such that

       A1: x = y & (B + y) c= X or x = y & (B + y) c= Y;

      (B + y) c= (X \/ Y) by A1, XBOOLE_0:def 3;

      hence thesis by A1;

    end;

    theorem :: MATHMORP:32

    ((X \/ Y) (+) B) = ((X (+) B) \/ (Y (+) B))

    proof

      thus ((X \/ Y) (+) B) c= ((X (+) B) \/ (Y (+) B))

      proof

        let x be object;

        assume x in ((X \/ Y) (+) B);

        then

        consider y1,y2 be Point of T such that

         A1: x = (y1 + y2) and

         A2: y1 in (X \/ Y) and

         A3: y2 in B;

        y1 in X or y1 in Y by A2, XBOOLE_0:def 3;

        then x in { (y3 + y4) where y3,y4 be Point of T : y3 in X & y4 in B } or x in { (y3 + y4) where y3,y4 be Point of T : y3 in Y & y4 in B } by A1, A3;

        hence thesis by XBOOLE_0:def 3;

      end;

      let x be object;

      assume x in ((X (+) B) \/ (Y (+) B));

      then x in (X (+) B) or x in (Y (+) B) by XBOOLE_0:def 3;

      then

      consider y1,y2 be Point of T such that

       A4: x = (y1 + y2) & y1 in X & y2 in B or x = (y1 + y2) & y1 in Y & y2 in B;

      y1 in (X \/ Y) by A4, XBOOLE_0:def 3;

      hence thesis by A4;

    end;

    theorem :: MATHMORP:33

    ((X /\ Y) (-) B) = ((X (-) B) /\ (Y (-) B))

    proof

      thus ((X /\ Y) (-) B) c= ((X (-) B) /\ (Y (-) B))

      proof

        let x be object;

        assume x in ((X /\ Y) (-) B);

        then

        consider y be Point of T such that

         A1: x = y and

         A2: (B + y) c= (X /\ Y);

        (B + y) c= Y by A2, XBOOLE_1: 18;

        then

         A3: x in { y1 where y1 be Point of T : (B + y1) c= Y } by A1;

        (B + y) c= X by A2, XBOOLE_1: 18;

        then x in { y1 where y1 be Point of T : (B + y1) c= X } by A1;

        hence thesis by A3, XBOOLE_0:def 4;

      end;

      let x be object;

      assume

       A4: x in ((X (-) B) /\ (Y (-) B));

      then x in (X (-) B) by XBOOLE_0:def 4;

      then

      consider y be Point of T such that

       A5: x = y and

       A6: (B + y) c= X;

      x in (Y (-) B) by A4, XBOOLE_0:def 4;

      then

       A7: ex y2 be Point of T st x = y2 & (B + y2) c= Y;

      (B + y) c= (X /\ Y) by A5, A6, A7, XBOOLE_0:def 4;

      hence thesis by A5;

    end;

    theorem :: MATHMORP:34

    

     Th34: ((X /\ Y) (+) B) c= ((X (+) B) /\ (Y (+) B))

    proof

      let x be object;

      assume x in ((X /\ Y) (+) B);

      then

      consider y1,y2 be Point of T such that

       A1: x = (y1 + y2) and

       A2: y1 in (X /\ Y) and

       A3: y2 in B;

      y1 in Y by A2, XBOOLE_0:def 4;

      then

       A4: x in { (y3 + y4) where y3,y4 be Point of T : y3 in Y & y4 in B } by A1, A3;

      y1 in X by A2, XBOOLE_0:def 4;

      then x in { (y3 + y4) where y3,y4 be Point of T : y3 in X & y4 in B } by A1, A3;

      hence thesis by A4, XBOOLE_0:def 4;

    end;

    theorem :: MATHMORP:35

    (B (+) (X /\ Y)) c= ((B (+) X) /\ (B (+) Y))

    proof

      (B (+) (X /\ Y)) = ((X /\ Y) (+) B) by Th12;

      then (B (+) (X /\ Y)) c= ((X (+) B) /\ (Y (+) B)) by Th34;

      then (B (+) (X /\ Y)) c= ((B (+) X) /\ (Y (+) B)) by Th12;

      hence thesis by Th12;

    end;

    theorem :: MATHMORP:36

    ((B (-) X) \/ (B (-) Y)) c= (B (-) (X /\ Y))

    proof

      let x be object;

      assume x in ((B (-) X) \/ (B (-) Y));

      then x in (B (-) X) or x in (B (-) Y) by XBOOLE_0:def 3;

      then

      consider y be Point of T such that

       A1: x = y & (X + y) c= B or x = y & (Y + y) c= B;

      ((X + y) /\ (Y + y)) c= B

      proof

        let a be object;

        assume

         A2: a in ((X + y) /\ (Y + y));

        then

         A3: a in (X + y) by XBOOLE_0:def 4;

        

         A4: a in (Y + y) by A2, XBOOLE_0:def 4;

        per cases by A1;

          suppose (X + y) c= B;

          hence thesis by A3;

        end;

          suppose (Y + y) c= B;

          hence thesis by A4;

        end;

      end;

      then ((X /\ Y) + y) c= B by Th28;

      hence thesis by A1;

    end;

    theorem :: MATHMORP:37

    

     Th37: (((X ` ) (-) B) ` ) = (X (+) (B ! ))

    proof

      thus (((X ` ) (-) B) ` ) c= (X (+) (B ! ))

      proof

        let x be object;

        assume

         A1: x in (((X ` ) (-) B) ` );

        then

        reconsider x1 = x as Point of T;

         not x in ((X ` ) (-) B) by A1, XBOOLE_0:def 5;

        then not (B + x1) c= (X ` );

        then (B + x1) meets X by SUBSET_1: 23;

        then

        consider y be object such that

         A2: y in (B + x1) and

         A3: y in X by XBOOLE_0: 3;

        reconsider y1 = y as Point of T by A2;

        consider b1 be Point of T such that

         A4: y = (b1 + x1) & b1 in B by A2;

        x1 = (y1 - b1) & ( - b1) in (B ! ) by A4, Lm2;

        hence thesis by A3;

      end;

      let x be object;

      assume x in (X (+) (B ! ));

      then

      consider x1,b1 be Point of T such that

       A5: x = (x1 + b1) and

       A6: x1 in X and

       A7: b1 in (B ! );

      reconsider xx = x as Point of T by A5;

      consider b2 be Point of T such that

       A8: b1 = ( - b2) and

       A9: b2 in B by A7;

      x = (x1 - b2) by A5, A8;

      then

       A10: (xx + b2) = x1 by Lm2;

      (b2 + xx) in { (pb + xx) where pb be Point of T : pb in B } by A9;

      then

       A11: (B + xx) meets X by A6, A10, XBOOLE_0: 3;

       not xx in ((X ` ) (-) B)

      proof

        assume xx in ((X ` ) (-) B);

        then ex yy be Point of T st xx = yy & (B + yy) c= (X ` );

        hence contradiction by A11, SUBSET_1: 23;

      end;

      hence thesis by XBOOLE_0:def 5;

    end;

    theorem :: MATHMORP:38

    

     Th38: ((X (-) B) ` ) = ((X ` ) (+) (B ! ))

    proof

      thus ((X (-) B) ` ) c= ((X ` ) (+) (B ! ))

      proof

        let x be object;

        assume

         A1: x in ((X (-) B) ` );

        then

        reconsider x1 = x as Point of T;

         not x in (X (-) B) by A1, XBOOLE_0:def 5;

        then not (B + x1) c= X;

        then (B + x1) meets (X ` ) by SUBSET_1: 24;

        then

        consider y be object such that

         A2: y in (B + x1) and

         A3: y in (X ` ) by XBOOLE_0: 3;

        reconsider y1 = y as Point of T by A2;

        consider b1 be Point of T such that

         A4: y = (b1 + x1) & b1 in B by A2;

        x1 = (y1 - b1) & ( - b1) in (B ! ) by A4, Lm2;

        hence thesis by A3;

      end;

      let x be object;

      assume x in ((X ` ) (+) (B ! ));

      then

      consider x1,b1 be Point of T such that

       A5: x = (x1 + b1) and

       A6: x1 in (X ` ) and

       A7: b1 in (B ! );

      reconsider xx = x as Point of T by A5;

      consider q be Point of T such that

       A8: b1 = ( - q) and

       A9: q in B by A7;

      xx = (x1 - q) by A5, A8;

      then

       A10: (xx + q) = x1 by Lm2;

      (q + xx) in { (q1 + xx) where q1 be Point of T : q1 in B } by A9;

      then

       A11: (B + xx) meets (X ` ) by A6, A10, XBOOLE_0: 3;

       not xx in (X (-) B)

      proof

        assume xx in (X (-) B);

        then ex yy be Point of T st xx = yy & (B + yy) c= X;

        hence contradiction by A11, SUBSET_1: 24;

      end;

      hence thesis by XBOOLE_0:def 5;

    end;

    begin

    definition

      let T be non empty addLoopStr, X,B be Subset of T;

      :: MATHMORP:def4

      func X (O) B -> Subset of T equals ((X (-) B) (+) B);

      coherence ;

    end

    definition

      let T be non empty addLoopStr, X,B be Subset of T;

      :: MATHMORP:def5

      func X (o) B -> Subset of T equals ((X (+) B) (-) B);

      coherence ;

    end

    theorem :: MATHMORP:39

    (((X ` ) (O) (B ! )) ` ) = (X (o) B)

    proof

      (((X ` ) (O) (B ! )) ` ) = ((((((X ` ) (-) (B ! )) ` ) (-) B) ` ) ` ) by Th37

      .= ((X (+) ((B ! ) ! )) (-) B) by Th37

      .= ((X (+) B) (-) B) by Th1;

      hence thesis;

    end;

    theorem :: MATHMORP:40

    (((X ` ) (o) (B ! )) ` ) = (X (O) B)

    proof

      (((X ` ) (o) (B ! )) ` ) = ((((X ` ) (+) (B ! )) ` ) (+) ((B ! ) ! )) by Th38

      .= ((((X ` ) (+) (B ! )) ` ) (+) B) by Th1

      .= ((((X (-) B) ` ) ` ) (+) B) by Th38;

      hence thesis;

    end;

    theorem :: MATHMORP:41

    

     Th41: (X (O) B) c= X & X c= (X (o) B)

    proof

      thus (X (O) B) c= X

      proof

        let x be object;

        assume x in (X (O) B);

        then

        consider y1,y2 be Point of T such that

         A1: x = (y1 + y2) and

         A2: y1 in (X (-) B) and

         A3: y2 in B;

        consider y be Point of T such that

         A4: y1 = y and

         A5: (B + y) c= X by A2;

        x in (B + y) by A1, A3, A4;

        hence thesis by A5;

      end;

      thus thesis by Th20;

    end;

    theorem :: MATHMORP:42

    

     Th42: (X (O) X) = X

    proof

      thus (X (O) X) c= X by Th41;

      let x be object;

      assume

       A1: x in X;

      then

      reconsider x1 = x as Point of T;

      (X + ( 0. T)) c= X by Th21;

      then ( 0. T) in (X (-) X);

      then (x1 + ( 0. T)) in ((X (-) X) (+) X) by A1;

      hence thesis;

    end;

    theorem :: MATHMORP:43

    ((X (O) B) (-) B) c= (X (-) B) & ((X (O) B) (+) B) c= (X (+) B)

    proof

      (X (O) B) c= X by Th41;

      hence thesis by Th9;

    end;

    theorem :: MATHMORP:44

    (X (-) B) c= ((X (o) B) (-) B) & (X (+) B) c= ((X (o) B) (+) B)

    proof

      X c= (X (o) B) by Th41;

      hence thesis by Th9;

    end;

    theorem :: MATHMORP:45

    

     Th45: X c= Y implies (X (O) B) c= (Y (O) B) & (X (o) B) c= (Y (o) B)

    proof

      assume

       A1: X c= Y;

      thus (X (O) B) c= (Y (O) B)

      proof

        let x be object;

        assume x in (X (O) B);

        then

        consider x2,b2 be Point of T such that

         A2: x = (x2 + b2) and

         A3: x2 in (X (-) B) and

         A4: b2 in B;

        consider y be Point of T such that

         A5: x2 = y and

         A6: (B + y) c= X by A3;

        (B + y) c= Y by A1, A6;

        then x2 in { y1 where y1 be Point of T : (B + y1) c= Y } by A5;

        hence thesis by A2, A4;

      end;

      let x be object;

      assume x in (X (o) B);

      then

      consider x2 be Point of T such that

       A7: x = x2 and

       A8: (B + x2) c= (X (+) B);

      (X (+) B) c= (Y (+) B) by A1, Th9;

      then (B + x2) c= (Y (+) B) by A8;

      hence thesis by A7;

    end;

    theorem :: MATHMORP:46

    

     Th46: ((X + p) (O) Y) = ((X (O) Y) + p)

    proof

      

      thus ((X + p) (O) Y) = (((X (-) Y) + p) (+) Y) by Th14

      .= ((X (O) Y) + p) by Th15;

    end;

    theorem :: MATHMORP:47

    ((X + p) (o) Y) = ((X (o) Y) + p)

    proof

      

      thus ((X + p) (o) Y) = (((X (+) Y) + p) (-) Y) by Th15

      .= ((X (o) Y) + p) by Th14;

    end;

    theorem :: MATHMORP:48

    C c= B implies (X (O) B) c= ((X (-) C) (+) B)

    proof

      assume

       A1: C c= B;

      let x be object;

      assume x in (X (O) B);

      then

      consider x1,b1 be Point of T such that

       A2: x = (x1 + b1) and

       A3: x1 in (X (-) B) and

       A4: b1 in B;

      consider x2 be Point of T such that

       A5: x1 = x2 and

       A6: (B + x2) c= X by A3;

      (C + x2) c= (B + x2) by A1, Th3;

      then (C + x2) c= X by A6;

      then x1 in (X (-) C) by A5;

      hence thesis by A2, A4;

    end;

    theorem :: MATHMORP:49

    B c= C implies (X (o) B) c= ((X (+) C) (-) B)

    proof

      assume B c= C;

      then

       A1: (X (+) B) c= (X (+) C) by Th10;

      let x be object;

      assume x in (X (o) B);

      then

      consider x2 be Point of T such that

       A2: x = x2 and

       A3: (B + x2) c= (X (+) B);

      (B + x2) c= (X (+) C) by A3, A1;

      hence thesis by A2;

    end;

    theorem :: MATHMORP:50

    

     Th50: (X (+) Y) = ((X (o) Y) (+) Y) & (X (-) Y) = ((X (O) Y) (-) Y)

    proof

      ((X (o) Y) (+) Y) = ((X (+) Y) (O) Y);

      then

       A1: ((X (o) Y) (+) Y) c= (X (+) Y) by Th41;

      X c= (X (o) Y) by Th41;

      then (X (+) Y) c= ((X (o) Y) (+) Y) by Th9;

      hence (X (+) Y) = ((X (o) Y) (+) Y) by A1;

      ((X (O) Y) (-) Y) = ((X (-) Y) (o) Y);

      hence (X (-) Y) c= ((X (O) Y) (-) Y) by Th41;

      (X (O) Y) c= X by Th41;

      hence thesis by Th9;

    end;

    theorem :: MATHMORP:51

    (X (+) Y) = ((X (+) Y) (O) Y) & (X (-) Y) = ((X (-) Y) (o) Y)

    proof

      ((X (+) Y) (O) Y) = ((X (o) Y) (+) Y);

      hence (X (+) Y) = ((X (+) Y) (O) Y) by Th50;

      ((X (-) Y) (o) Y) = ((X (O) Y) (-) Y);

      hence thesis by Th50;

    end;

    theorem :: MATHMORP:52

    ((X (O) B) (O) B) = (X (O) B)

    proof

      thus ((X (O) B) (O) B) c= (X (O) B) by Th41;

      let x be object;

      assume x in (X (O) B);

      then

      consider x1,b1 be Point of T such that

       A1: x = (x1 + b1) and

       A2: x1 in (X (-) B) and

       A3: b1 in B;

      consider x2 be Point of T such that

       A4: x1 = x2 and

       A5: (B + x2) c= X by A2;

      ((B + x2) (O) B) c= (X (O) B) by A5, Th45;

      then ((B (O) B) + x2) c= (X (O) B) by Th46;

      then (B + x2) c= (X (O) B) by Th42;

      then x1 in { x4 where x4 be Point of T : (B + x4) c= (X (O) B) } by A4;

      hence thesis by A1, A3;

    end;

    theorem :: MATHMORP:53

    ((X (o) B) (o) B) = (X (o) B) by Th50;

    theorem :: MATHMORP:54

    (X (O) B) c= ((X \/ Y) (O) B)

    proof

      X c= (X \/ Y) by XBOOLE_1: 7;

      hence thesis by Th45;

    end;

    theorem :: MATHMORP:55

    B = (B (O) B1) implies (X (O) B) c= (X (O) B1)

    proof

      assume

       A1: B = (B (O) B1);

      let x be object;

      assume x in (X (O) B);

      then

      consider x1,b1 be Point of T such that

       A2: x = (x1 + b1) and

       A3: x1 in (X (-) B) and

       A4: b1 in B;

      consider x2 be Point of T such that

       A5: x1 = x2 & (B + x2) c= X by A3;

      consider x3,b2 be Point of T such that

       A6: b1 = (x3 + b2) and

       A7: x3 in (B (-) B1) and

       A8: b2 in B1 by A1, A4;

      consider x4 be Point of T such that

       A9: x3 = x4 and

       A10: (B1 + x4) c= B by A7;

      ((B1 + x4) + x2) c= (B + x2) by A10, Th3;

      then ((B1 + x3) + x1) c= X by A5, A9;

      then (B1 + (x3 + x1)) c= X by Th16;

      then (x1 + x3) in (X (-) B1);

      then ((x1 + x3) + b2) in ((X (-) B1) (+) B1) by A8;

      hence thesis by A2, A6, RLVECT_1:def 3;

    end;

    begin

    definition

      let t be Real, T be non empty RLSStruct, A be Subset of T;

      :: MATHMORP:def6

      func t (.) A -> Subset of T equals { (t * a) where a be Point of T : a in A };

      coherence

      proof

        now

          let x be object;

          assume x in { (t * a) where a be Point of T : a in A };

          then ex q be Point of T st x = (t * q) & q in A;

          hence x in the carrier of T;

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    reserve t,s,r1 for Real;

    theorem :: MATHMORP:56

    for X be Subset of T st X = {} holds ( 0 (.) X) = {}

    proof

      let X be Subset of T;

      assume

       A1: X = {} ;

      now

        given x be object such that

         A2: x in ( 0 (.) X);

        ex a be Point of T st x = ( 0 * a) & a in X by A2;

        hence contradiction by A1;

      end;

      hence thesis by XBOOLE_0:def 1;

    end;

    reserve n for Element of NAT ;

    reserve X,Y,B1,B2 for Subset of ( TOP-REAL n);

    reserve x,y for Point of ( TOP-REAL n);

    theorem :: MATHMORP:57

    for X be non empty Subset of ( TOP-REAL n) holds ( 0 (.) X) = {( 0. ( TOP-REAL n))}

    proof

      set T = ( TOP-REAL n);

      let X be non empty Subset of ( TOP-REAL n);

      thus ( 0 (.) X) c= {( 0. T)}

      proof

        let x be object;

        assume x in ( 0 (.) X);

        then ex a be Point of T st x = ( 0 * a) & a in X;

        then x = ( 0. T) by RLVECT_1: 10;

        hence thesis by ZFMISC_1: 31;

      end;

      let x be object;

      set d = the Element of X;

      reconsider d1 = d as Point of T;

      assume x in {( 0. T)};

      then {x} c= {( 0. T)} by ZFMISC_1: 31;

      then x = ( 0. T) by ZFMISC_1: 18;

      then x = ( 0 * d1) by RLVECT_1: 10;

      hence thesis;

    end;

    theorem :: MATHMORP:58

    

     Th58: (1 (.) X) = X

    proof

      thus (1 (.) X) c= X

      proof

        let x be object;

        assume x in (1 (.) X);

        then ex z be Point of ( TOP-REAL n) st x = (1 * z) & z in X;

        hence thesis by RLVECT_1:def 8;

      end;

      let x be object;

      assume

       A1: x in X;

      then

      reconsider x1 = x as Point of ( TOP-REAL n);

      x1 = (1 * x1) by RLVECT_1:def 8;

      hence thesis by A1;

    end;

    theorem :: MATHMORP:59

    (2 (.) X) c= (X (+) X)

    proof

      let x be object;

      assume x in (2 (.) X);

      then

      consider z be Point of ( TOP-REAL n) such that

       A1: x = (2 * z) and

       A2: z in X;

      x = ((1 + 1) * z) by A1

      .= ((1 * z) + (1 * z)) by RLVECT_1:def 6

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

      .= (z + z) by RLVECT_1:def 8;

      hence thesis by A2;

    end;

    theorem :: MATHMORP:60

    

     Th60: ((t * s) (.) X) = (t (.) (s (.) X))

    proof

      thus ((t * s) (.) X) c= (t (.) (s (.) X))

      proof

        let x be object;

        assume x in ((t * s) (.) X);

        then

        consider z be Point of ( TOP-REAL n) such that

         A1: x = ((t * s) * z) & z in X;

        x = (t * (s * z)) & (s * z) in (s (.) X) by A1, RLVECT_1:def 7;

        hence thesis;

      end;

      let x be object;

      assume x in (t (.) (s (.) X));

      then

      consider z be Point of ( TOP-REAL n) such that

       A2: x = (t * z) and

       A3: z in (s (.) X);

      consider z1 be Point of ( TOP-REAL n) such that

       A4: z = (s * z1) and

       A5: z1 in X by A3;

      x = ((t * s) * z1) by A2, A4, RLVECT_1:def 7;

      hence thesis by A5;

    end;

    theorem :: MATHMORP:61

    

     Th61: X c= Y implies (t (.) X) c= (t (.) Y)

    proof

      assume

       A1: X c= Y;

      let x be object;

      assume x in (t (.) X);

      then ex a be Point of ( TOP-REAL n) st x = (t * a) & a in X;

      hence thesis by A1;

    end;

    theorem :: MATHMORP:62

    

     Th62: (t (.) (X + x)) = ((t (.) X) + (t * x))

    proof

      thus (t (.) (X + x)) c= ((t (.) X) + (t * x))

      proof

        let b be object;

        assume b in (t (.) (X + x));

        then

        consider a be Point of ( TOP-REAL n) such that

         A1: b = (t * a) and

         A2: a in (X + x);

        consider x1 be Point of ( TOP-REAL n) such that

         A3: a = (x1 + x) and

         A4: x1 in X by A2;

        

         A5: (t * x1) in (t (.) X) by A4;

        b = ((t * x1) + (t * x)) by A1, A3, RLVECT_1:def 5;

        hence thesis by A5;

      end;

      let b be object;

      assume b in ((t (.) X) + (t * x));

      then

      consider x1 be Point of ( TOP-REAL n) such that

       A6: b = (x1 + (t * x)) and

       A7: x1 in (t (.) X);

      consider a be Point of ( TOP-REAL n) such that

       A8: x1 = (t * a) and

       A9: a in X by A7;

      

       A10: (a + x) in (X + x) by A9;

      b = (t * (a + x)) by A6, A8, RLVECT_1:def 5;

      hence thesis by A10;

    end;

    theorem :: MATHMORP:63

    

     Th63: (t (.) (X (+) Y)) = ((t (.) X) (+) (t (.) Y))

    proof

      thus (t (.) (X (+) Y)) c= ((t (.) X) (+) (t (.) Y))

      proof

        let b be object;

        assume b in (t (.) (X (+) Y));

        then

        consider a be Point of ( TOP-REAL n) such that

         A1: b = (t * a) and

         A2: a in (X (+) Y);

        consider x,y be Point of ( TOP-REAL n) such that

         A3: a = (x + y) and

         A4: x in X & y in Y by A2;

        

         A5: (t * x) in (t (.) X) & (t * y) in (t (.) Y) by A4;

        b = ((t * x) + (t * y)) by A1, A3, RLVECT_1:def 5;

        hence thesis by A5;

      end;

      let b be object;

      assume b in ((t (.) X) (+) (t (.) Y));

      then

      consider x,y be Point of ( TOP-REAL n) such that

       A6: b = (x + y) and

       A7: x in (t (.) X) and

       A8: y in (t (.) Y);

      consider y1 be Point of ( TOP-REAL n) such that

       A9: y = (t * y1) and

       A10: y1 in Y by A8;

      consider x1 be Point of ( TOP-REAL n) such that

       A11: x = (t * x1) and

       A12: x1 in X by A7;

      

       A13: (x1 + y1) in (X (+) Y) by A12, A10;

      b = (t * (x1 + y1)) by A6, A11, A9, RLVECT_1:def 5;

      hence thesis by A13;

    end;

    theorem :: MATHMORP:64

    

     Th64: t <> 0 implies (t (.) (X (-) Y)) = ((t (.) X) (-) (t (.) Y))

    proof

      assume

       A1: t <> 0 ;

      thus (t (.) (X (-) Y)) c= ((t (.) X) (-) (t (.) Y))

      proof

        let b be object;

        assume b in (t (.) (X (-) Y));

        then

        consider a be Point of ( TOP-REAL n) such that

         A2: b = (t * a) and

         A3: a in (X (-) Y);

        consider x be Point of ( TOP-REAL n) such that

         A4: a = x and

         A5: (Y + x) c= X by A3;

        (t (.) (Y + x)) c= (t (.) X) by A5, Th61;

        then ((t (.) Y) + (t * x)) c= (t (.) X) by Th62;

        hence thesis by A2, A4;

      end;

      let b be object;

      assume b in ((t (.) X) (-) (t (.) Y));

      then

      consider x be Point of ( TOP-REAL n) such that

       A6: b = x and

       A7: ((t (.) Y) + x) c= (t (.) X);

      ((1 / t) (.) ((t (.) Y) + x)) c= ((1 / t) (.) (t (.) X)) by A7, Th61;

      then ((1 / t) (.) ((t (.) Y) + x)) c= (((1 / t) * t) (.) X) by Th60;

      then (((1 / t) (.) (t (.) Y)) + ((1 / t) * x)) c= (((1 / t) * t) (.) X) by Th62;

      then ((((1 / t) * t) (.) Y) + ((1 / t) * x)) c= (((1 / t) * t) (.) X) by Th60;

      then ((1 (.) Y) + ((1 / t) * x)) c= (((1 / t) * t) (.) X) by A1, XCMPLX_1: 87;

      then ((1 (.) Y) + ((1 / t) * x)) c= (1 (.) X) by A1, XCMPLX_1: 87;

      then (Y + ((1 / t) * x)) c= (1 (.) X) by Th58;

      then (Y + ((1 / t) * x)) c= X by Th58;

      then ((1 / t) * x) in { z where z be Point of ( TOP-REAL n) : (Y + z) c= X };

      then (t * ((1 / t) * x)) in { (t * a1) where a1 be Point of ( TOP-REAL n) : a1 in (X (-) Y) };

      then (((1 / t) * t) * x) in (t (.) (X (-) Y)) by RLVECT_1:def 7;

      then (1 * x) in (t (.) (X (-) Y)) by A1, XCMPLX_1: 87;

      hence thesis by A6, RLVECT_1:def 8;

    end;

    theorem :: MATHMORP:65

    t <> 0 implies (t (.) (X (O) Y)) = ((t (.) X) (O) (t (.) Y))

    proof

      assume

       A1: t <> 0 ;

      (t (.) (X (O) Y)) = ((t (.) (X (-) Y)) (+) (t (.) Y)) by Th63

      .= (((t (.) X) (-) (t (.) Y)) (+) (t (.) Y)) by A1, Th64;

      hence thesis;

    end;

    theorem :: MATHMORP:66

    t <> 0 implies (t (.) (X (o) Y)) = ((t (.) X) (o) (t (.) Y))

    proof

      assume t <> 0 ;

      

      then (t (.) (X (o) Y)) = ((t (.) (X (+) Y)) (-) (t (.) Y)) by Th64

      .= (((t (.) X) (+) (t (.) Y)) (-) (t (.) Y)) by Th63;

      hence thesis;

    end;

    begin

    definition

      let T be non empty RLSStruct, X,B1,B2 be Subset of T;

      :: MATHMORP:def7

      func X (*) (B1,B2) -> Subset of T equals ((X (-) B1) /\ ((X ` ) (-) B2));

      coherence ;

    end

    definition

      let T be non empty RLSStruct, X,B1,B2 be Subset of T;

      :: MATHMORP:def8

      func X (&) (B1,B2) -> Subset of T equals (X \/ (X (*) (B1,B2)));

      coherence ;

    end

    definition

      let T be non empty RLSStruct, X,B1,B2 be Subset of T;

      :: MATHMORP:def9

      func X (@) (B1,B2) -> Subset of T equals (X \ (X (*) (B1,B2)));

      coherence ;

    end

    theorem :: MATHMORP:67

    B1 = {} implies (X (*) (B1,B2)) = ((X ` ) (-) B2)

    proof

      assume B1 = {} ;

      then (X (*) (B1,B2)) = (((X ` ) (-) B2) /\ the carrier of ( TOP-REAL n)) by Th8;

      hence thesis by XBOOLE_1: 28;

    end;

    theorem :: MATHMORP:68

    B2 = {} implies (X (*) (B1,B2)) = (X (-) B1)

    proof

      assume B2 = {} ;

      then (X (*) (B1,B2)) = ((X (-) B1) /\ the carrier of ( TOP-REAL n)) by Th8;

      hence thesis by XBOOLE_1: 28;

    end;

    theorem :: MATHMORP:69

    ( 0. ( TOP-REAL n)) in B1 implies (X (*) (B1,B2)) c= X

    proof

      assume

       A1: ( 0. ( TOP-REAL n)) in B1;

      let x be object;

      assume x in (X (*) (B1,B2));

      then x in (X (-) B1) by XBOOLE_0:def 4;

      then

      consider y be Point of ( TOP-REAL n) such that

       A2: x = y and

       A3: (B1 + y) c= X;

      (( 0. ( TOP-REAL n)) + y) in { (z + y) where z be Point of ( TOP-REAL n) : z in B1 } by A1;

      then x in (B1 + y) by A2;

      hence thesis by A3;

    end;

    theorem :: MATHMORP:70

    ( 0. ( TOP-REAL n)) in B2 implies ((X (*) (B1,B2)) /\ X) = {}

    proof

      assume

       A1: ( 0. ( TOP-REAL n)) in B2;

      now

        given x be object such that

         A2: x in ((X (*) (B1,B2)) /\ X);

        

         A3: x in X by A2, XBOOLE_0:def 4;

        x in (X (*) (B1,B2)) by A2, XBOOLE_0:def 4;

        then x in ((X ` ) (-) B2) by XBOOLE_0:def 4;

        then

        consider y be Point of ( TOP-REAL n) such that

         A4: x = y and

         A5: (B2 + y) c= (X ` );

        (( 0. ( TOP-REAL n)) + y) in { (z + y) where z be Point of ( TOP-REAL n) : z in B2 } by A1;

        then x in (B2 + y) by A4;

        hence contradiction by A3, A5, XBOOLE_0:def 5;

      end;

      hence thesis by XBOOLE_0:def 1;

    end;

    theorem :: MATHMORP:71

    ( 0. ( TOP-REAL n)) in B1 implies (X (&) (B1,B2)) = X

    proof

      assume

       A1: ( 0. ( TOP-REAL n)) in B1;

      thus (X (&) (B1,B2)) c= X

      proof

        let x be object;

        assume

         A2: x in (X (&) (B1,B2));

        per cases by A2, XBOOLE_0:def 3;

          suppose x in X;

          hence thesis;

        end;

          suppose x in (X (*) (B1,B2));

          then x in (X (-) B1) by XBOOLE_0:def 4;

          then

          consider y be Point of ( TOP-REAL n) such that

           A3: x = y and

           A4: (B1 + y) c= X;

          (( 0. ( TOP-REAL n)) + y) in { (z + y) where z be Point of ( TOP-REAL n) : z in B1 } by A1;

          then x in (B1 + y) by A3;

          hence thesis by A4;

        end;

      end;

      thus thesis by XBOOLE_1: 7;

    end;

    theorem :: MATHMORP:72

    ( 0. ( TOP-REAL n)) in B2 implies (X (@) (B1,B2)) = X

    proof

      assume

       A1: ( 0. ( TOP-REAL n)) in B2;

      thus (X (@) (B1,B2)) c= X by XBOOLE_0:def 5;

      let x be object;

      assume

       A2: x in X;

       not x in (X (*) (B1,B2))

      proof

        assume x in (X (*) (B1,B2));

        then x in ((X ` ) (-) B2) by XBOOLE_0:def 4;

        then

        consider y be Point of ( TOP-REAL n) such that

         A3: x = y and

         A4: (B2 + y) c= (X ` );

        (( 0. ( TOP-REAL n)) + y) in { (z + y) where z be Point of ( TOP-REAL n) : z in B2 } by A1;

        then x in (B2 + y) by A3;

        hence contradiction by A2, A4, XBOOLE_0:def 5;

      end;

      hence thesis by A2, XBOOLE_0:def 5;

    end;

    theorem :: MATHMORP:73

    (X (@) (B2,B1)) = (((X ` ) (&) (B1,B2)) ` )

    proof

      (((X ` ) (&) (B1,B2)) ` ) = (((X \ (((X ` ) (-) B1) /\ (((X ` ) ` ) (-) B2))) ` ) ` ) by SUBSET_1: 14

      .= (X \ (X (*) (B2,B1)));

      hence thesis;

    end;

    begin

    theorem :: MATHMORP:74

    

     Th74: for V be RealLinearSpace, B be Subset of V holds B is convex iff for x,y be Point of V, r be Real st 0 <= r & r <= 1 & x in B & y in B holds ((r * x) + ((1 - r) * y)) in B

    proof

      let V be RealLinearSpace, B be Subset of V;

      thus B is convex implies for x,y be Point of V, r be Real st 0 <= r & r <= 1 & x in B & y in B holds ((r * x) + ((1 - r) * y)) in B

      proof

        assume

         A1: B is convex;

        for x,y be Point of V, r be Real st 0 <= r & r <= 1 & x in B & y in B holds ((r * x) + ((1 - r) * y)) in B

        proof

          let x,y be Point of V, r be Real;

          assume that

           A2: 0 <= r & r <= 1 and

           A3: x in B & y in B;

          (((1 - r) * y) + (r * x)) in { (((1 - r1) * y) + (r1 * x)) where r1 be Real : 0 <= r1 & r1 <= 1 } by A2;

          then

           A4: (((1 - r) * y) + (r * x)) in ( LSeg (x,y)) by RLTOPSP1:def 2;

          ( LSeg (x,y)) c= B by A1, A3, JORDAN1:def 1;

          hence thesis by A4;

        end;

        hence thesis;

      end;

      (for x,y be Point of V, r be Real st 0 <= r & r <= 1 & x in B & y in B holds ((r * x) + ((1 - r) * y)) in B) implies B is convex

      proof

        assume

         A5: for x,y be Point of V, r be Real st 0 <= r & r <= 1 & x in B & y in B holds ((r * x) + ((1 - r) * y)) in B;

        for x,y be Point of V st x in B & y in B holds ( LSeg (x,y)) c= B

        proof

          let x,y be Point of V;

          assume

           A6: x in B & y in B;

          let p be object;

          assume p in ( LSeg (x,y));

          then p in { (((1 - r1) * y) + (r1 * x)) where r1 be Real : 0 <= r1 & r1 <= 1 } by RLTOPSP1:def 2;

          then ex r1 be Real st p = (((1 - r1) * y) + (r1 * x)) & 0 <= r1 & r1 <= 1;

          hence thesis by A5, A6;

        end;

        hence thesis by RLTOPSP1: 22;

      end;

      hence thesis;

    end;

    definition

      let V be RealLinearSpace, B be Subset of V;

      :: original: convex

      redefine

      :: MATHMORP:def10

      attr B is convex means for x,y be Point of V, r be Real st 0 <= r & r <= 1 & x in B & y in B holds ((r * x) + ((1 - r) * y)) in B;

      compatibility by Th74;

    end

    reserve n for Element of NAT ;

    reserve X,B for Subset of ( TOP-REAL n);

    theorem :: MATHMORP:75

    X is convex implies (X ! ) is convex

    proof

      assume

       A1: X is convex;

      for x,y be Point of ( TOP-REAL n), r be Real st 0 <= r & r <= 1 & x in (X ! ) & y in (X ! ) holds ((r * x) + ((1 - r) * y)) in (X ! )

      proof

        let x,y be Point of ( TOP-REAL n), r be Real;

        assume that

         A2: 0 <= r & r <= 1 and

         A3: x in (X ! ) and

         A4: y in (X ! );

        consider x2 be Point of ( TOP-REAL n) such that

         A5: y = ( - x2) and

         A6: x2 in X by A4;

        consider x1 be Point of ( TOP-REAL n) such that

         A7: x = ( - x1) and

         A8: x1 in X by A3;

        ((r * x1) + ((1 - r) * x2)) in X by A1, A2, A8, A6;

        then ( - ((r * x1) + ((1 - r) * x2))) in (X ! );

        then (( - (r * x1)) - ((1 - r) * x2)) in (X ! ) by RLVECT_1: 30;

        then ((r * ( - x1)) + ( - ((1 - r) * x2))) in (X ! ) by RLVECT_1: 25;

        hence thesis by A7, A5, RLVECT_1: 25;

      end;

      hence thesis;

    end;

    theorem :: MATHMORP:76

    

     Th76: X is convex & B is convex implies (X (+) B) is convex & (X (-) B) is convex

    proof

      assume that

       A1: X is convex and

       A2: B is convex;

      for x,y be Point of ( TOP-REAL n), r be Real st 0 <= r & r <= 1 & x in (X (+) B) & y in (X (+) B) holds ((r * x) + ((1 - r) * y)) in (X (+) B)

      proof

        let x,y be Point of ( TOP-REAL n), r be Real;

        assume that

         A3: 0 <= r & r <= 1 and

         A4: x in (X (+) B) and

         A5: y in (X (+) B);

        consider x2,b2 be Point of ( TOP-REAL n) such that

         A6: y = (x2 + b2) and

         A7: x2 in X & b2 in B by A5;

        consider x1,b1 be Point of ( TOP-REAL n) such that

         A8: x = (x1 + b1) and

         A9: x1 in X & b1 in B by A4;

        ((r * x1) + ((1 - r) * x2)) in X & ((r * b1) + ((1 - r) * b2)) in B by A1, A2, A3, A9, A7;

        then (((r * x1) + ((1 - r) * x2)) + ((r * b1) + ((1 - r) * b2))) in { (x3 + b3) where x3,b3 be Point of ( TOP-REAL n) : x3 in X & b3 in B };

        then ((((r * x1) + ((1 - r) * x2)) + (r * b1)) + ((1 - r) * b2)) in (X (+) B) by RLVECT_1:def 3;

        then ((((r * x1) + (r * b1)) + ((1 - r) * x2)) + ((1 - r) * b2)) in (X (+) B) by RLVECT_1:def 3;

        then (((r * x1) + (r * b1)) + (((1 - r) * x2) + ((1 - r) * b2))) in (X (+) B) by RLVECT_1:def 3;

        then ((r * (x1 + b1)) + (((1 - r) * x2) + ((1 - r) * b2))) in (X (+) B) by RLVECT_1:def 5;

        hence thesis by A8, A6, RLVECT_1:def 5;

      end;

      hence (X (+) B) is convex;

      for x,y be Point of ( TOP-REAL n), r be Real st 0 <= r & r <= 1 & x in (X (-) B) & y in (X (-) B) holds ((r * x) + ((1 - r) * y)) in (X (-) B)

      proof

        let x,y be Point of ( TOP-REAL n), r be Real;

        assume that

         A10: 0 <= r & r <= 1 and

         A11: x in (X (-) B) & y in (X (-) B);

        

         A12: (ex x1 be Point of ( TOP-REAL n) st x = x1 & (B + x1) c= X) & ex y1 be Point of ( TOP-REAL n) st y = y1 & (B + y1) c= X by A11;

        (B + ((r * x) + ((1 - r) * y))) c= X

        proof

          let b1 be object;

          assume b1 in (B + ((r * x) + ((1 - r) * y)));

          then

          consider b be Point of ( TOP-REAL n) such that

           A13: b1 = (b + ((r * x) + ((1 - r) * y))) and

           A14: b in B;

          (b + x) in (B + x) & (b + y) in { (b2 + y) where b2 be Point of ( TOP-REAL n) : b2 in B } by A14;

          then ((r * (b + x)) + ((1 - r) * (b + y))) in X by A1, A10, A12;

          then (((r * b) + (r * x)) + ((1 - r) * (b + y))) in X by RLVECT_1:def 5;

          then (((r * b) + (r * x)) + (((1 - r) * b) + ((1 - r) * y))) in X by RLVECT_1:def 5;

          then ((((r * b) + (r * x)) + ((1 - r) * b)) + ((1 - r) * y)) in X by RLVECT_1:def 3;

          then ((((r * b) + (r * x)) + ((1 * b) - (r * b))) + ((1 - r) * y)) in X by RLVECT_1: 35;

          then (((((r * b) + (r * x)) + (1 * b)) - (r * b)) + ((1 - r) * y)) in X by RLVECT_1:def 3;

          then (((((r * x) + (1 * b)) + (r * b)) - (r * b)) + ((1 - r) * y)) in X by RLVECT_1:def 3;

          then (((r * x) + (1 * b)) + ((1 - r) * y)) in X by RLVECT_4: 1;

          then ((1 * b) + ((r * x) + ((1 - r) * y))) in X by RLVECT_1:def 3;

          hence thesis by A13, RLVECT_1:def 8;

        end;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: MATHMORP:77

    X is convex & B is convex implies (X (O) B) is convex & (X (o) B) is convex

    proof

      assume that

       A1: X is convex and

       A2: B is convex;

      (X (-) B) is convex by A1, A2, Th76;

      hence (X (O) B) is convex by A2, Th76;

      (X (+) B) is convex by A1, A2, Th76;

      hence thesis by A2, Th76;

    end;

    theorem :: MATHMORP:78

    B is convex & 0 < t & 0 < s implies ((s + t) (.) B) = ((s (.) B) (+) (t (.) B))

    proof

      assume that

       A1: B is convex and

       A2: 0 < t & 0 < s;

      thus ((s + t) (.) B) c= ((s (.) B) (+) (t (.) B))

      proof

        let x be object;

        assume x in ((s + t) (.) B);

        then

        consider b be Point of ( TOP-REAL n) such that

         A3: x = ((s + t) * b) and

         A4: b in B;

        

         A5: (t * b) in (t (.) B) by A4;

        x = ((s * b) + (t * b)) & (s * b) in (s (.) B) by A3, A4, RLVECT_1:def 6;

        hence thesis by A5;

      end;

      let x be object;

      assume x in ((s (.) B) (+) (t (.) B));

      then

      consider s1,s2 be Point of ( TOP-REAL n) such that

       A6: x = (s1 + s2) and

       A7: s1 in (s (.) B) and

       A8: s2 in (t (.) B);

      consider b2 be Point of ( TOP-REAL n) such that

       A9: s2 = (t * b2) and

       A10: b2 in B by A8;

      consider b1 be Point of ( TOP-REAL n) such that

       A11: s1 = (s * b1) and

       A12: b1 in B by A7;

      (s / (s + t)) < ((s + t) / (s + t)) by A2, XREAL_1: 29, XREAL_1: 74;

      then (s / (s + t)) < 1 by A2, XCMPLX_1: 60;

      then (((s / (s + t)) * b1) + ((1 - (s / (s + t))) * b2)) in B by A1, A2, A12, A10;

      then ((s + t) * (((s / (s + t)) * b1) + ((1 - (s / (s + t))) * b2))) in { ((s + t) * zz) where zz be Point of ( TOP-REAL n) : zz in B };

      then (((s + t) * ((s / (s + t)) * b1)) + ((s + t) * ((1 - (s / (s + t))) * b2))) in ((s + t) (.) B) by RLVECT_1:def 5;

      then ((((s + t) * (s / (s + t))) * b1) + ((s + t) * ((1 - (s / (s + t))) * b2))) in ((s + t) (.) B) by RLVECT_1:def 7;

      then ((((s + t) * (s / (s + t))) * b1) + (((s + t) * (1 - (s / (s + t)))) * b2)) in ((s + t) (.) B) by RLVECT_1:def 7;

      then ((s * b1) + (((s + t) * (1 - (s / (s + t)))) * b2)) in ((s + t) (.) B) by A2, XCMPLX_1: 87;

      then ((s * b1) + (((s + t) * (((s + t) / (s + t)) - (s / (s + t)))) * b2)) in ((s + t) (.) B) by A2, XCMPLX_1: 60;

      then ((s * b1) + (((s + t) * (((s + t) - s) / (s + t))) * b2)) in ((s + t) (.) B) by XCMPLX_1: 120;

      hence thesis by A2, A6, A11, A9, XCMPLX_1: 87;

    end;