measure6.miz



    begin

    theorem :: MEASURE6:1

    ex F be sequence of [: NAT , NAT :] st F is one-to-one & ( dom F) = NAT & ( rng F) = [: NAT , NAT :]

    proof

      consider F be Function such that

       A1: F is one-to-one and

       A2: ( dom F) = NAT & ( rng F) = [: NAT , NAT :] by CARD_4: 5, WELLORD2:def 4;

      F is sequence of [: NAT , NAT :] by A2, FUNCT_2: 1;

      hence thesis by A1, A2;

    end;

    theorem :: MEASURE6:2

    for F be sequence of ExtREAL st F is nonnegative holds 0. <= ( SUM F)

    proof

      let F be sequence of ExtREAL ;

      assume F is nonnegative;

      then 0. <= (( Ser F) . 0 ) by SUPINF_2: 40;

      hence thesis by FUNCT_2: 4, XXREAL_2: 4;

    end;

    theorem :: MEASURE6:3

    for F be sequence of ExtREAL , x be R_eal st (ex n be Element of NAT st x <= (F . n)) & F is nonnegative holds x <= ( SUM F)

    proof

      let F be sequence of ExtREAL ;

      let x be R_eal;

      assume that

       A1: ex n be Element of NAT st x <= (F . n) and

       A2: F is nonnegative;

      consider n be Element of NAT such that

       A3: x <= (F . n) by A1;

      

       A4: (( Ser F) . n) <= ( SUM F) by FUNCT_2: 4, XXREAL_2: 4;

      per cases by NAT_1: 6;

        suppose n = 0 ;

        then (( Ser F) . n) = (F . n) by SUPINF_2:def 11;

        hence thesis by A3, A4, XXREAL_0: 2;

      end;

        suppose ex k be Nat st n = (k + 1);

        then

        consider k be Nat such that

         A5: n = (k + 1);

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

        

         A6: 0. <= (( Ser F) . k) by A2, SUPINF_2: 40;

        (( Ser F) . n) = ((( Ser F) . k) + (F . (k + 1))) by A5, SUPINF_2:def 11;

        then ( 0. + x) <= (( Ser F) . n) by A3, A5, A6, XXREAL_3: 36;

        then x <= (( Ser F) . n) by XXREAL_3: 4;

        hence thesis by A4, XXREAL_0: 2;

      end;

    end;

    definition

      ::$Canceled

    end

    theorem :: MEASURE6:4

    for eps be ExtReal st 0. < eps holds ex F be sequence of ExtREAL st (for n be Nat holds 0. < (F . n)) & ( SUM F) < eps

    proof

      defpred P[ set, set, set] means for a,b be R_eal, s be Nat holds (s = $1 & a = $2 & b = $3 implies b = (a / 2));

      let eps be ExtReal;

      assume 0. < eps;

      then

      consider x0 be Real such that

       A1: 0. < x0 and

       A2: x0 < eps by XXREAL_3: 3;

      consider x be Real such that

       A3: 0. < x and

       A4: (x + x qua ExtReal) < x0 by A1, XXREAL_3: 50;

      reconsider x as Element of ExtREAL by XXREAL_0:def 1;

      

       A5: for n be Nat holds for x be Element of ExtREAL holds ex y be Element of ExtREAL st P[n, x, y]

      proof

        let n be Nat;

        let x be Element of ExtREAL ;

        reconsider m = (x / 2) as Element of ExtREAL by XXREAL_0:def 1;

        take m;

        thus thesis;

      end;

      consider F be sequence of ExtREAL such that

       A6: (F . 0 ) = x & for n be Nat holds P[n, (F . n), (F . (n + 1))] from RECDEF_1:sch 2( A5);

      take F;

      defpred P[ Nat] means 0. < (F . $1);

      

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

      proof

        let k be Nat;

        assume

         A8: 0. < (F . k);

        (F . (k + 1)) = ((F . k) / 2) by A6;

        hence thesis by A8;

      end;

      

       A9: P[ 0 ] by A3, A6;

      thus

       A10: for n be Nat holds P[n] from NAT_1:sch 2( A9, A7);

      then for n be Element of NAT holds 0. <= (F . n);

      then

       A11: F is nonnegative by SUPINF_2: 39;

      for s be ExtReal holds s in ( rng ( Ser F)) implies s <= x0

      proof

        defpred P[ Nat] means ((( Ser F) . $1) + (F . $1)) < x0;

        let s be ExtReal;

        assume s in ( rng ( Ser F));

        then

        consider n be object such that

         A12: n in ( dom ( Ser F)) and

         A13: s = (( Ser F) . n) by FUNCT_1:def 3;

        reconsider n as Element of NAT by A12;

        

         A14: for l be Nat st P[l] holds P[(l + 1)]

        proof

          let l be Nat;

          (F . (l + 1)) = ((F . l) / 2) by A6;

          then

           A15: ((( Ser F) . l) + ((F . (l + 1)) + (F . (l + 1)))) <= ((( Ser F) . l) + (F . l)) by XXREAL_3: 105;

           0. <= (( Ser F) . l) & 0. <= (F . (l + 1)) by A10, A11, SUPINF_2: 40;

          then

           A16: ((( Ser F) . (l + 1)) + (F . (l + 1))) = (((( Ser F) . l) + (F . (l + 1))) + (F . (l + 1))) & (((( Ser F) . l) + (F . (l + 1))) + (F . (l + 1))) <= ((( Ser F) . l) + (F . l)) by A15, SUPINF_2:def 11, XXREAL_3: 44;

          assume ((( Ser F) . l) + (F . l)) < x0;

          hence thesis by A16, XXREAL_0: 2;

        end;

        

         A17: P[ 0 ] by A4, A6, SUPINF_2:def 11;

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

        then

         A18: ((( Ser F) . n) + (F . n)) < x0;

         0. <= (( Ser F) . n) & 0. <= (F . n) by A10, A11, SUPINF_2: 40;

        hence thesis by A13, A18, XXREAL_3: 48;

      end;

      then x0 is UpperBound of ( rng ( Ser F)) by XXREAL_2:def 1;

      then

       A19: ( sup ( rng ( Ser F))) <= x0 by XXREAL_2:def 3;

      per cases by A19, XXREAL_0: 1;

        suppose ( SUM F) < x0;

        hence thesis by A2, XXREAL_0: 2;

      end;

        suppose ( SUM F) = x0;

        hence thesis by A2;

      end;

    end;

    theorem :: MEASURE6:5

    for eps be ExtReal, X be non empty Subset of ExtREAL st 0. < eps & ( inf X) is Real holds ex x be ExtReal st x in X & x < (( inf X) + eps)

    proof

      let eps be ExtReal;

      let X be non empty Subset of ExtREAL ;

      assume that

       A1: 0. < eps and

       A2: ( inf X) is Real;

      

       A3: ( inf X) in REAL by A2, XREAL_0:def 1;

      assume not ex x be ExtReal st x in X & x < (( inf X) + eps);

      then (( inf X) + eps) is LowerBound of X by XXREAL_2:def 2;

      then

       A4: (( inf X) + eps) <= ( inf X) by XXREAL_2:def 4;

      per cases by XXREAL_0: 4;

        suppose eps < +infty ;

        then

        reconsider a = ( inf X), b = eps as Element of REAL by A1, A3, XXREAL_0: 48;

        (( inf X) + eps) = (a + b) by SUPINF_2: 1;

        then b <= (a - a) by A4, XREAL_1: 19;

        hence thesis by A1;

      end;

        suppose eps = +infty ;

        then (( inf X) + eps) = +infty by A3, XXREAL_3:def 2;

        hence thesis by A3, A4, XXREAL_0: 4;

      end;

    end;

    theorem :: MEASURE6:6

    for eps be ExtReal, X be non empty Subset of ExtREAL st 0. < eps & ( sup X) is Real holds ex x be ExtReal st x in X & (( sup X) - eps) < x

    proof

      let eps be ExtReal;

      let X be non empty Subset of ExtREAL ;

      assume that

       A1: 0. < eps and

       A2: ( sup X) is Real;

      

       A3: ( sup X) in REAL by A2, XREAL_0:def 1;

      assume not ex x be ExtReal st x in X & (( sup X) - eps) < x;

      then (( sup X) - eps) is UpperBound of X by XXREAL_2:def 1;

      then

       A4: ( sup X) <= (( sup X) - eps) by XXREAL_2:def 3;

      per cases by XXREAL_0: 4;

        suppose eps < +infty ;

        then

        reconsider a = ( sup X), b = eps as Element of REAL by A1, A3, XXREAL_0: 48;

        a <= (a - b) by A4, SUPINF_2: 3;

        hence thesis by A1, XREAL_1: 44;

      end;

        suppose eps = +infty ;

        then (( sup X) - eps) = -infty by A3, XXREAL_3: 13;

        hence thesis by A3, A4, XXREAL_0: 6;

      end;

    end;

    theorem :: MEASURE6:7

    for F be sequence of ExtREAL st F is nonnegative & ( SUM F) < +infty holds for n be Element of NAT holds (F . n) in REAL

    proof

      let F be sequence of ExtREAL ;

      assume that

       A1: F is nonnegative and

       A2: ( SUM F) < +infty ;

      let n be Element of NAT ;

      defpred P[ Nat] means (F . $1) <= (( Ser F) . $1);

      

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

      proof

        let k be Nat;

        assume (F . k) <= (( Ser F) . k);

        reconsider x = (( Ser F) . k) as R_eal;

        (x + (F . (k + 1))) = (( Ser F) . (k + 1)) by SUPINF_2:def 11;

        hence thesis by A1, SUPINF_2: 40, XXREAL_3: 39;

      end;

      

       A4: P[ 0 ] by SUPINF_2:def 11;

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

      then

       A5: (F . n) <= (( Ser F) . n);

      (( Ser F) . n) <= ( SUM F) by FUNCT_2: 4, XXREAL_2: 4;

      then (F . n) <= ( SUM F) by A5, XXREAL_0: 2;

      then

       A6: (F . n) < +infty by A2, XXREAL_0: 2;

      

       A7: 0 in REAL by XREAL_0:def 1;

       0. = 0 & 0. <= (F . n) by A1, SUPINF_2: 39;

      hence thesis by A6, XXREAL_0: 46, A7;

    end;

    registration

      cluster non empty interval for Subset of REAL ;

      existence

      proof

        take ( [#] REAL );

        thus thesis;

      end;

    end

    theorem :: MEASURE6:8

    for A be non empty Interval, a be ExtReal st ex b be ExtReal st a <= b & A = ].a, b.[ holds a = ( inf A) by XXREAL_1: 28, XXREAL_2: 28;

    theorem :: MEASURE6:9

    for A be non empty Interval, a be ExtReal st ex b be ExtReal st a <= b & A = ].a, b.] holds a = ( inf A) by XXREAL_1: 26, XXREAL_2: 27;

    theorem :: MEASURE6:10

    for A be non empty Interval, a be ExtReal st ex b be ExtReal st a <= b & A = [.a, b.] holds a = ( inf A) by XXREAL_2: 25;

    theorem :: MEASURE6:11

    

     Th11: for A be non empty Interval, a be ExtReal st ex b be ExtReal st a <= b & A = [.a, b.[ holds a = ( inf A)

    proof

      let A be non empty Interval, IT be ExtReal;

      given b be ExtReal such that

       A1: IT <= b and

       A2: A = [.IT, b.[;

      IT <> b by A2;

      then IT < b by A1, XXREAL_0: 1;

      hence thesis by A2, XXREAL_2: 26;

    end;

    theorem :: MEASURE6:12

    for A be non empty Interval, b be ExtReal st ex a be ExtReal st a <= b & A = ].a, b.[ holds b = ( sup A) by XXREAL_1: 28, XXREAL_2: 32;

    theorem :: MEASURE6:13

    

     Th13: for A be non empty Interval, b be ExtReal st ex a be ExtReal st a <= b & A = ].a, b.] holds b = ( sup A)

    proof

      let A be non empty Interval, IT be ExtReal;

      given a be ExtReal such that

       A1: a <= IT and

       A2: A = ].a, IT.];

      a <> IT by A2;

      then a < IT by A1, XXREAL_0: 1;

      hence thesis by A2, XXREAL_2: 30;

    end;

    theorem :: MEASURE6:14

    for A be non empty Interval, b be ExtReal st ex a be ExtReal st a <= b & A = [.a, b.] holds b = ( sup A) by XXREAL_2: 29;

    theorem :: MEASURE6:15

    

     Th15: for A be non empty Interval, b be ExtReal st ex a be ExtReal st a <= b & A = [.a, b.[ holds b = ( sup A)

    proof

      let A be non empty Interval, IT be ExtReal;

      given a be ExtReal such that

       A1: a <= IT and

       A2: A = [.a, IT.[;

      a <> IT by A2;

      then a < IT by A1, XXREAL_0: 1;

      hence thesis by A2, XXREAL_2: 31;

    end;

    theorem :: MEASURE6:16

    for A be non empty Interval st A is open_interval holds A = ].( inf A), ( sup A).[

    proof

      let A be non empty Interval;

      assume A is open_interval;

      then

      consider a,b be R_eal such that

       A1: A = ].a, b.[ by MEASURE5:def 2;

      ( sup A) = b by A1, XXREAL_1: 28, XXREAL_2: 32;

      hence thesis by A1, XXREAL_1: 28, XXREAL_2: 28;

    end;

    theorem :: MEASURE6:17

    for A be non empty Interval st A is closed_interval holds A = [.( inf A), ( sup A).]

    proof

      let A be non empty Interval;

      assume A is closed_interval;

      then

      consider a,b be Real such that

       A1: A = [.a, b.] by MEASURE5:def 3;

      

       A2: a <= b by A1, XXREAL_1: 29;

      reconsider b as R_eal by XXREAL_0:def 1;

      ( sup A) = b by A1, A2, XXREAL_2: 29;

      hence thesis by A1, A2, XXREAL_2: 25;

    end;

    theorem :: MEASURE6:18

    for A be non empty Interval st A is right_open_interval holds A = [.( inf A), ( sup A).[

    proof

      let A be non empty Interval;

      assume A is right_open_interval;

      then

      consider a be Real, b be R_eal such that

       A1: A = [.a, b.[ by MEASURE5:def 4;

      reconsider a as R_eal by XXREAL_0:def 1;

      

       A2: a <= b by A1, XXREAL_1: 27;

      then ( sup A) = b by A1, Th15;

      hence thesis by A1, A2, Th11;

    end;

    theorem :: MEASURE6:19

    for A be non empty Interval st A is left_open_interval holds A = ].( inf A), ( sup A).]

    proof

      let A be non empty Interval;

      assume A is left_open_interval;

      then

      consider a be R_eal, b be Real such that

       A1: A = ].a, b.] by MEASURE5:def 5;

      

       A2: a <= b by A1, XXREAL_1: 26;

      reconsider b as R_eal by XXREAL_0:def 1;

      ( sup A) = b by A2, A1, Th13;

      hence thesis by A1, XXREAL_1: 26, XXREAL_2: 27;

    end;

    theorem :: MEASURE6:20

    for A,B be non empty Interval, a,b be Real st a in A & b in B & ( sup A) <= ( inf B) holds a <= b

    proof

      let A,B be non empty Interval, a,b be Real;

      assume that

       A1: a in A and

       A2: b in B;

      

       A3: ( inf B) <= b by A2, XXREAL_2: 3;

      assume

       A4: ( sup A) <= ( inf B);

      a <= ( sup A) by A1, XXREAL_2: 4;

      then a <= ( inf B) by A4, XXREAL_0: 2;

      hence thesis by A3, XXREAL_0: 2;

    end;

    theorem :: MEASURE6:21

    for A,B be real-membered set holds for y be Real holds y in (B ++ A) iff ex x,z be Real st x in B & z in A & y = (x + z)

    proof

      let A,B be real-membered set;

      let y be Real;

      hereby

        assume y in (B ++ A);

        then

        consider x,w be Complex such that

         A1: y = (x + w) & x in B & w in A;

        reconsider x, w as Real by A1;

        take x, w;

        thus x in B & w in A & y = (x + w) by A1;

      end;

      given w,z be Real such that

       A2: w in B & z in A & y = (w + z);

      thus thesis by A2;

    end;

    theorem :: MEASURE6:22

    for A,B be non empty Interval holds ( sup A) = ( inf B) & (( sup A) in A or ( inf B) in B) implies (A \/ B) is Interval by XXREAL_2:def 5, XXREAL_2:def 6, XXREAL_2: 90, XXREAL_2: 91;

    definition

      let A be real-membered set;

      let x be Real;

      :: original: ++

      redefine

      func x ++ A -> Subset of REAL ;

      coherence by MEMBERED: 3;

    end

    

     Lm1: for A be real-membered set, x be Real holds for y be Real holds y in (x ++ A) iff ex z be Real st z in A & y = (x + z)

    proof

      let A be real-membered set, x be Real;

      let y be Real;

      hereby

        assume y in (x ++ A);

        then

        consider w be Complex such that

         A1: y = (x + w) & w in A by MEMBER_1: 143;

        reconsider w as Real by A1;

        take w;

        thus w in A & y = (x + w) by A1;

      end;

      given z be Real such that

       A2: z in A & y = (x + z);

      thus thesis by A2, MEMBER_1: 141;

    end;

    theorem :: MEASURE6:23

    

     Th23: for A be Subset of REAL , x be Real holds (( - x) ++ (x ++ A)) = A

    proof

      let A be Subset of REAL , x be Real;

      thus (( - x) ++ (x ++ A)) c= A

      proof

        let y be object;

        assume

         A1: y in (( - x) ++ (x ++ A));

        then

        reconsider y as Real;

        consider z be Real such that

         A2: z in (x ++ A) and

         A3: y = (( - x) + z) by A1, Lm1;

        ex t be Real st t in A & z = (x + t) by A2, Lm1;

        hence thesis by A3;

      end;

      let y be object;

      assume

       A4: y in A;

      then

      reconsider y as Real;

      reconsider t = (y - ( - x)) as Real;

      reconsider z = (t - x) as Real;

      

       A5: z = (( - x) + t);

      t in (x ++ A) by A4, Lm1;

      hence thesis by A5, Lm1;

    end;

    theorem :: MEASURE6:24

    for x be Real, A be Subset of REAL st A = REAL holds (x ++ A) = A

    proof

      let x be Real, A be Subset of REAL ;

      assume

       A1: A = REAL ;

      A c= (x ++ A)

      proof

        let y be object;

        assume y in A;

        then

        reconsider y as Real;

        reconsider z = (y - x) as Element of REAL by XREAL_0:def 1;

        y = (x + z);

        hence thesis by A1, Lm1;

      end;

      hence thesis by A1;

    end;

    theorem :: MEASURE6:25

    for x be Real holds (x ++ {} ) = {} ;

    theorem :: MEASURE6:26

    

     Th26: for A be Interval, x be Real holds A is open_interval iff (x ++ A) is open_interval

    proof

      let A be Interval, x be Real;

      reconsider y = ( - x) as Element of REAL by XREAL_0:def 1;

      

       A1: for B be Interval, y be Real st B is open_interval holds (y ++ B) is open_interval

      proof

        let B be Interval;

        let y be Real;

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

        reconsider z = y as R_eal by XXREAL_0:def 1;

        assume B is open_interval;

        then

        consider a,b be R_eal such that

         A2: B = ].a, b.[ by MEASURE5:def 2;

        reconsider s = (z + a), t = (z + b) as R_eal;

        (y ++ B) = ].s, t.[

        proof

          thus (y ++ B) c= ].s, t.[

          proof

            let c be object;

            assume

             A3: c in (y ++ B);

            then

            reconsider c as Element of REAL ;

            consider d be Real such that

             A4: d in B and

             A5: c = (y + d) by A3, Lm1;

            reconsider d1 = d as R_eal by XXREAL_0:def 1;

            a < d1 by A2, A4, MEASURE5:def 1;

            then

             A6: s < (z + d1) by XXREAL_3: 43;

            d1 < b by A2, A4, MEASURE5:def 1;

            then

             A7: (z + d1) < t by XXREAL_3: 43;

            (z + d1) = c by A5, SUPINF_2: 1;

            hence thesis by A6, A7;

          end;

          let c be object;

          assume

           A8: c in ].s, t.[;

          then

          reconsider c as Element of REAL ;

          reconsider c1 = c as R_eal by XXREAL_0:def 1;

          

           A9: c = (y + (c - y));

          c1 < (z + b) by A8, MEASURE5:def 1;

          then (c1 - z) < ((b + z) - z) by XXREAL_3: 43;

          then

           A10: (c1 - z) < b by XXREAL_3: 22;

          (z + a) < c1 by A8, MEASURE5:def 1;

          then ((a + z) - z) < (c1 - z) by XXREAL_3: 43;

          then

           A11: a < (c1 - z) by XXREAL_3: 22;

          (c1 - z) = (c - y) by SUPINF_2: 3;

          then (c - y) in B by A2, A11, A10;

          hence thesis by A9, Lm1;

        end;

        hence thesis by MEASURE5:def 2;

      end;

      hence A is open_interval implies (x ++ A) is open_interval;

      assume

       A12: (x ++ A) is open_interval;

      then

      reconsider B = (x ++ A) as Interval;

      (y ++ B) = A by Th23;

      hence thesis by A1, A12;

    end;

    theorem :: MEASURE6:27

    

     Th27: for A be Interval, x be Real holds A is closed_interval iff (x ++ A) is closed_interval

    proof

      let A be Interval;

      let x be Real;

      

       A1: for B be Interval, y be Real st B is closed_interval holds (y ++ B) is closed_interval

      proof

        let B be Interval;

        let y be Real;

        reconsider y as Real;

        reconsider z = y as R_eal by XXREAL_0:def 1;

        assume B is closed_interval;

        then

        consider a1,b1 be Real such that

         A2: B = [.a1, b1.] by MEASURE5:def 3;

        reconsider a = a1, b = b1 as R_eal by XXREAL_0:def 1;

        reconsider s = (z + a), t = (z + b) as R_eal;

        (y ++ B) = [.s, t.]

        proof

          thus (y ++ B) c= [.s, t.]

          proof

            let c be object;

            assume

             A3: c in (y ++ B);

            then

            reconsider c as Real;

            consider d be Real such that

             A4: d in B and

             A5: c = (y + d) by A3, Lm1;

            reconsider d1 = d as R_eal by XXREAL_0:def 1;

            a <= d1 by A2, A4, XXREAL_1: 1;

            then

             A6: s <= (z + d1) by XXREAL_3: 36;

            d1 <= b by A2, A4, XXREAL_1: 1;

            then

             A7: (z + d1) <= t by XXREAL_3: 36;

            (z + d1) = c by A5, SUPINF_2: 1;

            hence thesis by A6, A7, XXREAL_1: 1;

          end;

          reconsider a, b as R_eal;

          let c be object;

          assume

           A8: c in [.s, t.];

          then

          reconsider c as Real;

          reconsider c1 = c as R_eal by XXREAL_0:def 1;

          

           A9: c = (y + (c - y));

          c1 <= (z + b) by A8, XXREAL_1: 1;

          then (c1 - z) <= ((b + z) - z) by XXREAL_3: 36;

          then

           A10: (c1 - z) <= b by XXREAL_3: 22;

          (z + a) <= c1 by A8, XXREAL_1: 1;

          then ((a + z) - z) <= (c1 - z) by XXREAL_3: 36;

          then

           A11: a <= (c1 - z) by XXREAL_3: 22;

          (c1 - z) = (c - y) by SUPINF_2: 3;

          then (c - y) in B by A2, A11, A10;

          hence thesis by A9, Lm1;

        end;

        hence thesis by MEASURE5:def 3;

      end;

      (x ++ A) is closed_interval implies A is closed_interval

      proof

        reconsider y = ( - x) as Real;

        assume

         A12: (x ++ A) is closed_interval;

        then

        reconsider B = (x ++ A) as Interval;

        (y ++ B) = A by Th23;

        hence thesis by A1, A12;

      end;

      hence thesis by A1;

    end;

    theorem :: MEASURE6:28

    

     Th28: for A be Interval, x be Real holds A is right_open_interval iff (x ++ A) is right_open_interval

    proof

      let A be Interval;

      let x be Real;

      

       A1: for B be Interval, y be Real st B is right_open_interval holds (y ++ B) is right_open_interval

      proof

        let B be Interval;

        let y be Real;

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

        reconsider z = y as R_eal by XXREAL_0:def 1;

        assume B is right_open_interval;

        then

        consider a1 be Real, b be R_eal such that

         A2: B = [.a1, b.[ by MEASURE5:def 4;

        reconsider a = a1 as R_eal by XXREAL_0:def 1;

        reconsider s = (z + a), t = (z + b) as R_eal;

        (y ++ B) = [.s, t.[

        proof

          thus (y ++ B) c= [.s, t.[

          proof

            let c be object;

            assume

             A3: c in (y ++ B);

            then

            reconsider c as Element of REAL ;

            consider d be Real such that

             A4: d in B and

             A5: c = (y + d) by A3, Lm1;

            reconsider d1 = d as R_eal by XXREAL_0:def 1;

            a <= d1 by A2, A4, XXREAL_1: 3;

            then

             A6: s <= (z + d1) by XXREAL_3: 36;

            d1 < b by A2, A4, XXREAL_1: 3;

            then

             A7: (z + d1) < t by XXREAL_3: 43;

            (z + d1) = c by A5, SUPINF_2: 1;

            hence thesis by A6, A7, XXREAL_1: 3;

          end;

          let c be object;

          assume

           A8: c in [.s, t.[;

          then

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

          reconsider c1 = c as R_eal by XXREAL_0:def 1;

          

           A9: c = (y + (c - y));

          c1 < (z + b) by A8, XXREAL_1: 3;

          then (c1 - z) < ((b + z) - z) by XXREAL_3: 43;

          then

           A10: (c1 - z) < b by XXREAL_3: 22;

          (z + a) <= c1 by A8, XXREAL_1: 3;

          then ((a + z) - z) <= (c1 - z) by XXREAL_3: 36;

          then

           A11: a <= (c1 - z) by XXREAL_3: 22;

          (c1 - z) = (c - y) by SUPINF_2: 3;

          then (c - y) in B by A2, A11, A10;

          hence thesis by A9, Lm1;

        end;

        hence thesis by MEASURE5:def 4;

      end;

      (x ++ A) is right_open_interval implies A is right_open_interval

      proof

        reconsider y = ( - x) as Real;

        assume

         A12: (x ++ A) is right_open_interval;

        then

        reconsider B = (x ++ A) as Interval;

        (y ++ B) = A by Th23;

        hence thesis by A1, A12;

      end;

      hence thesis by A1;

    end;

    theorem :: MEASURE6:29

    

     Th29: for A be Interval, x be Real holds A is left_open_interval iff (x ++ A) is left_open_interval

    proof

      let A be Interval, x be Real;

      

       A1: for B be Interval, y be Real st B is left_open_interval holds (y ++ B) is left_open_interval

      proof

        let B be Interval, y be Real;

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

        reconsider z = y as R_eal by XXREAL_0:def 1;

        assume B is left_open_interval;

        then

        consider a be R_eal, b1 be Real such that

         A2: B = ].a, b1.] by MEASURE5:def 5;

        reconsider b = b1 as R_eal by XXREAL_0:def 1;

        set s = (z + a), t = (z + b);

        (y ++ B) = ].s, t.]

        proof

          thus (y ++ B) c= ].s, t.]

          proof

            let c be object;

            assume

             A3: c in (y ++ B);

            then

            reconsider c as Element of REAL ;

            consider d be Real such that

             A4: d in B and

             A5: c = (y + d) by A3, Lm1;

            reconsider d1 = d as R_eal by XXREAL_0:def 1;

            a < d1 by A2, A4, XXREAL_1: 2;

            then

             A6: s < (z + d1) by XXREAL_3: 43;

            d1 <= b by A2, A4, XXREAL_1: 2;

            then

             A7: (z + d1) <= t by XXREAL_3: 36;

            (z + d1) = c by A5, SUPINF_2: 1;

            hence thesis by A6, A7, XXREAL_1: 2;

          end;

          let c be object;

          assume

           A8: c in ].s, t.];

          then

          reconsider c as Real;

          reconsider c1 = c as R_eal by XXREAL_0:def 1;

          

           A9: c = (y + (c - y));

          c1 <= (z + b) by A8, XXREAL_1: 2;

          then (c1 - z) <= ((b + z) - z) by XXREAL_3: 36;

          then

           A10: (c1 - z) <= b by XXREAL_3: 22;

          (z + a) < c1 by A8, XXREAL_1: 2;

          then ((a + z) - z) < (c1 - z) by XXREAL_3: 43;

          then

           A11: a < (c1 - z) by XXREAL_3: 22;

          (c1 - z) = (c - y) by SUPINF_2: 3;

          then (c - y) in B by A2, A11, A10;

          hence thesis by A9, Lm1;

        end;

        hence thesis by MEASURE5:def 5;

      end;

      (x ++ A) is left_open_interval implies A is left_open_interval

      proof

        reconsider y = ( - x) as Real;

        assume

         A12: (x ++ A) is left_open_interval;

        then

        reconsider B = (x ++ A) as Interval;

        (y ++ B) = A by Th23;

        hence thesis by A1, A12;

      end;

      hence thesis by A1;

    end;

    theorem :: MEASURE6:30

    for A be Interval, x be Real holds (x ++ A) is Interval

    proof

      let A be Interval, x be Real;

      per cases by MEASURE5: 1;

        suppose A is open_interval;

        then (x ++ A) is open_interval by Th26;

        hence thesis;

      end;

        suppose A is closed_interval;

        then (x ++ A) is closed_interval by Th27;

        hence thesis;

      end;

        suppose A is right_open_interval;

        then (x ++ A) is right_open_interval by Th28;

        hence thesis;

      end;

        suppose A is left_open_interval;

        then (x ++ A) is left_open_interval by Th29;

        hence thesis;

      end;

    end;

    theorem :: MEASURE6:31

    

     Th31: for A be real-membered set, x be Real, y be R_eal st x = y holds ( sup (x ++ A)) = (y + ( sup A))

    proof

      let A be real-membered set, x be Real, y be R_eal such that

       A1: x = y;

      

       A2: for z be UpperBound of (x ++ A) holds (y + ( sup A)) <= z

      proof

        let z be UpperBound of (x ++ A);

        reconsider zz = z as R_eal by XXREAL_0:def 1;

        (zz - y) is UpperBound of A

        proof

          let u be ExtReal;

          reconsider uu = u as R_eal by XXREAL_0:def 1;

          assume

           A3: u in A;

          then

          reconsider u1 = u as Real;

          (y + uu) = (x + u1) by A1, XXREAL_3:def 2;

          then (y + uu) in (x ++ A) by A3, Lm1;

          then (y + uu) <= z by XXREAL_2:def 1;

          hence thesis by A1, XXREAL_3: 45;

        end;

        then ( sup A) <= (zz - y) by XXREAL_2:def 3;

        hence thesis by A1, XXREAL_3: 45;

      end;

      (y + ( sup A)) is UpperBound of (x ++ A)

      proof

        let z be ExtReal;

        assume z in (x ++ A);

        then

        consider a be Real such that

         A4: a in A and

         A5: z = (x + a) by Lm1;

        reconsider b = a as R_eal by XXREAL_0:def 1;

        

         A6: a <= ( sup A) by A4, XXREAL_2: 4;

        ex a,c be Complex st y = a & b = c & (y + b) = (a + c) by A1, XXREAL_3:def 2;

        hence thesis by A1, A5, A6, XXREAL_3: 36;

      end;

      hence thesis by A2, XXREAL_2:def 3;

    end;

    theorem :: MEASURE6:32

    

     Th32: for A be real-membered set, x be Real, y be R_eal st x = y holds ( inf (x ++ A)) = (y + ( inf A))

    proof

      let A be real-membered set, x be Real, y be R_eal such that

       A1: x = y;

      

       A2: for z be LowerBound of (x ++ A) holds z <= (y + ( inf A))

      proof

        let z be LowerBound of (x ++ A);

        reconsider zz = z as R_eal by XXREAL_0:def 1;

        (zz - y) is LowerBound of A

        proof

          let u be ExtReal;

          reconsider uu = u as R_eal by XXREAL_0:def 1;

          assume

           A3: u in A;

          then

          reconsider u1 = u as Real;

          (y + uu) = (x + u1) by A1, XXREAL_3:def 2;

          then (y + uu) in (x ++ A) by A3, Lm1;

          then z <= (y + uu) by XXREAL_2:def 2;

          hence thesis by A1, XXREAL_3: 42;

        end;

        then (zz - y) <= ( inf A) by XXREAL_2:def 4;

        hence thesis by A1, XXREAL_3: 41;

      end;

      (y + ( inf A)) is LowerBound of (x ++ A)

      proof

        let z be ExtReal;

        assume z in (x ++ A);

        then

        consider a be Real such that

         A4: a in A and

         A5: z = (x + a) by Lm1;

        reconsider b = a as R_eal by XXREAL_0:def 1;

        

         A6: ( inf A) <= a by A4, XXREAL_2: 3;

        ex a,c be Complex st y = a & b = c & (y + b) = (a + c) by A1, XXREAL_3:def 2;

        hence thesis by A1, A5, A6, XXREAL_3: 36;

      end;

      hence thesis by A2, XXREAL_2:def 4;

    end;

    theorem :: MEASURE6:33

    for A be Interval, x be Real holds ( diameter A) = ( diameter (x ++ A))

    proof

      let A be Interval, x be Real;

      per cases ;

        suppose A is empty;

        hence thesis;

      end;

        suppose

         A1: A is non empty;

        then

        consider y be Real such that

         A2: y in A;

        reconsider y as Real;

        

         A3: (x + y) in (x ++ A) by A2, Lm1;

        reconsider y = x as R_eal by XXREAL_0:def 1;

        

        thus ( diameter A) = (( sup A) - ( inf A)) by A1, MEASURE5:def 6

        .= ((y + ( sup A)) - (y + ( inf A))) by XXREAL_3: 33

        .= (( sup (x ++ A)) - (y + ( inf A))) by Th31

        .= (( sup (x ++ A)) - ( inf (x ++ A))) by Th32

        .= ( diameter (x ++ A)) by A3, MEASURE5:def 6;

      end;

    end;

    begin

    notation

      let X be set;

      synonym X is without_zero for X is with_non-empty_elements;

      antonym X is with_zero for X is with_non-empty_elements;

    end

    definition

      let X be set;

      :: original: without_zero

      redefine

      :: MEASURE6:def2

      attr X is without_zero means

      : Def1: not 0 in X;

      compatibility by SETFAM_1:def 8;

    end

    registration

      cluster REAL -> with_zero;

      coherence by XREAL_0:def 1;

      cluster NAT -> with_zero;

      coherence ;

    end

    registration

      cluster non empty without_zero for set;

      existence

      proof

        set s = {1};

        take s;

        thus s is non empty;

        thus thesis;

      end;

      cluster non empty with_zero for set;

      existence by Def1;

    end

    registration

      cluster non empty without_zero for Subset of REAL ;

      existence

      proof

        set s = {1 qua Real};

        take s;

        thus s is non empty;

        thus thesis;

      end;

      cluster non empty with_zero for Subset of REAL ;

      existence

      proof

        take ( [#] REAL );

        thus thesis;

      end;

    end

    theorem :: MEASURE6:34

    

     Th34: for F be set st F is non empty with_non-empty_elements c=-linear holds F is centered

    proof

      defpred P[ set] means $1 <> {} implies ex x be set st x in $1 & for y be set st y in $1 holds x c= y;

      let F be set;

      assume that

       A1: F is non empty and

       A2: F is with_non-empty_elements and

       A3: F is c=-linear;

      thus F <> {} by A1;

      let G be set;

      assume that

       A4: G <> {} and

       A5: G c= F and

       A6: G is finite;

       A7:

      now

        let x,B be set;

        assume that

         A8: x in G and

         A9: B c= G and

         A10: P[B];

        thus P[(B \/ {x})]

        proof

          assume (B \/ {x}) <> {} ;

          per cases ;

            suppose

             A11: B is empty;

            take x9 = x;

            thus x9 in (B \/ {x}) by A11, TARSKI:def 1;

            let y be set;

            thus thesis by A11, TARSKI:def 1;

          end;

            suppose B is non empty;

            then

            consider z be set such that

             A12: z in B and

             A13: for y be set st y in B holds z c= y by A10;

            thus ex x9 be set st x9 in (B \/ {x}) & for y be set st y in (B \/ {x}) holds x9 c= y

            proof

              z in G by A9, A12;

              then

               A14: (x,z) are_c=-comparable by A3, A5, A8, ORDINAL1:def 8;

              per cases by A14;

                suppose

                 A15: x c= z;

                take x9 = x;

                x9 in {x} by TARSKI:def 1;

                hence x9 in (B \/ {x}) by XBOOLE_0:def 3;

                let y be set;

                assume

                 A16: y in (B \/ {x});

                per cases by A16, XBOOLE_0:def 3;

                  suppose y in B;

                  then z c= y by A13;

                  hence thesis by A15;

                end;

                  suppose y in {x};

                  hence thesis by TARSKI:def 1;

                end;

              end;

                suppose

                 A17: z c= x;

                take x9 = z;

                thus x9 in (B \/ {x}) by A12, XBOOLE_0:def 3;

                let y be set;

                assume

                 A18: y in (B \/ {x});

                per cases by A18, XBOOLE_0:def 3;

                  suppose y in B;

                  hence thesis by A13;

                end;

                  suppose y in {x};

                  hence thesis by A17, TARSKI:def 1;

                end;

              end;

            end;

          end;

        end;

      end;

      

       A19: P[ {} ];

       P[G] from FINSET_1:sch 2( A6, A19, A7);

      then

      consider x be set such that

       A20: x in G and

       A21: for y be set st y in G holds x c= y by A4;

      consider xe be object such that

       A22: xe in x by A2, A5, A20, XBOOLE_0:def 1;

      now

        let y be set;

        assume y in G;

        then x c= y by A21;

        hence xe in y by A22;

      end;

      hence thesis by A4, SETFAM_1:def 1;

    end;

    registration

      let F be set;

      cluster non empty with_non-empty_elements c=-linear -> centered for Subset-Family of F;

      coherence by Th34;

    end

    registration

      let X,Y be non empty set, f be Function of X, Y;

      cluster (f .: X) -> non empty;

      coherence

      proof

        set x = the Element of X;

        

         A1: ( dom f) = X by FUNCT_2:def 1;

        thus thesis by A1;

      end;

    end

    definition

      let X,Y be set, f be Function of X, Y;

      :: MEASURE6:def3

      func " f -> Function of ( bool Y), ( bool X) means

      : Def2: for y be Subset of Y holds (it . y) = (f " y);

      existence

      proof

        deffunc F( Subset of Y) = (f " $1);

        thus ex T be Function of ( bool Y), ( bool X) st for y be Subset of Y holds (T . y) = F(y) from FUNCT_2:sch 4;

      end;

      uniqueness

      proof

        deffunc F( Subset of Y) = (f " $1);

        thus for T1,T2 be Function of ( bool Y), ( bool X) st (for y be Subset of Y holds (T1 . y) = F(y)) & (for y be Subset of Y holds (T2 . y) = F(y)) holds T1 = T2 from BINOP_2:sch 1;

      end;

    end

    theorem :: MEASURE6:35

    for X,Y,x be set, S be Subset-Family of Y, f be Function of X, Y st x in ( meet (( " f) .: S)) holds (f . x) in ( meet S)

    proof

      let X,Y,x be set, S be Subset-Family of Y, f be Function of X, Y;

      assume

       A1: x in ( meet (( " f) .: S));

       A2:

      now

        let SS be set;

        assume

         A3: SS in S;

        then (( " f) . SS) in (( " f) .: S) by FUNCT_2: 35;

        then

         A4: x in (( " f) . SS) by A1, SETFAM_1:def 1;

        (( " f) . SS) = (f " SS) by A3, Def2;

        hence (f . x) in SS by A4, FUNCT_1:def 7;

      end;

      (( " f) .: S) is non empty by A1, SETFAM_1:def 1;

      then S is non empty;

      hence thesis by A2, SETFAM_1:def 1;

    end;

    reserve r,s,t for Real;

    theorem :: MEASURE6:36

    

     Th36: ( |.r.| + |.s.|) = 0 implies r = 0

    proof

      set aa = |.r.|, ab = |.s.|;

      

       A1: 0 <= aa & 0 <= ab by COMPLEX1: 46;

      assume ( |.r.| + |.s.|) = 0 ;

      then aa = 0 by A1;

      hence thesis by ABSVALUE: 2;

    end;

    theorem :: MEASURE6:37

    

     Th37: r < s & s < t implies |.s.| < ( |.r.| + |.t.|)

    proof

      assume that

       A1: r < s and

       A2: s < t;

      per cases ;

        suppose

         A3: s < 0 ;

        ( - s) < ( - r) by A1, XREAL_1: 24;

        then

         A4: (( - s) + 0 ) < (( - r) + |.t.|) by COMPLEX1: 46, XREAL_1: 8;

        ( - s) = |.s.| by A3, ABSVALUE:def 1;

        hence thesis by A1, A3, A4, ABSVALUE:def 1;

      end;

        suppose

         A5: 0 <= s;

        

         A6: (s + 0 ) < (t + |.r.|) by A2, COMPLEX1: 46, XREAL_1: 8;

        s = |.s.| by A5, ABSVALUE:def 1;

        hence thesis by A2, A5, A6, ABSVALUE:def 1;

      end;

    end;

    reserve seq for Real_Sequence,

X,Y for Subset of REAL ;

    theorem :: MEASURE6:38

    

     Th38: seq is convergent & seq is non-zero & ( lim seq) = 0 implies (seq " ) is non bounded

    proof

      assume that

       A1: seq is convergent and

       A2: seq is non-zero and

       A3: ( lim seq) = 0 ;

      given r such that

       A4: for n be Nat holds ((seq " ) . n) < r;

      given s such that

       A5: for n be Nat holds s < ((seq " ) . n);

      set aa = |.r.|, ab = |.s.|;

      set rab = (1 / (aa + ab));

      

       A6: 0 <= aa & 0 <= ab by COMPLEX1: 46;

       A7:

      now

        let n be Element of NAT ;

        set g = (seq . n), t = ((seq " ) . n);

        set At = |.t.|;

        t = (1 / g) by VALUED_1: 10;

        then

         A8: At = (1 / |.g.|) by ABSVALUE: 7;

        (t " ) = ((g " ) " ) by VALUED_1: 10;

        then t <> 0 by A2, SEQ_1: 5, XCMPLX_1: 202;

        then

         A9: 0 < At by COMPLEX1: 47;

        s < t & t < r by A4, A5;

        then At < (aa + ab) by Th37;

        then (At " ) > ((aa + ab) " ) by A9, XREAL_1: 88;

        hence |.(seq . n).| > rab by A8;

      end;

      

       A10: ((seq " ) . 1) < r by A4;

      

       A11: s < ((seq " ) . 1) by A5;

      now

        assume 0 >= (aa + ab);

        then

         A12: (aa + ab) = 0 by A6;

        then r = 0 by Th36;

        hence contradiction by A11, A10, A12, Th36;

      end;

      then

      consider n be Nat such that

       A13: for m be Nat st n <= m holds |.((seq . m) - 0 ).| < rab by A1, A3, SEQ_2:def 7;

      

       A14: n in NAT by ORDINAL1:def 12;

       |.((seq . n) - 0 ).| < rab by A13;

      hence contradiction by A7, A14;

    end;

    theorem :: MEASURE6:39

    

     Th39: ( rng seq) is real-bounded iff seq is bounded

    proof

      thus ( rng seq) is real-bounded implies seq is bounded

      proof

        given s such that

         A1: s is LowerBound of ( rng seq);

        given t such that

         A2: t is UpperBound of ( rng seq);

        thus seq is bounded_above

        proof

          take (t + 1);

          let n be Nat;

          

           A3: n in NAT by ORDINAL1:def 12;

          (seq . n) <= t & t < (t + 1) by A2, FUNCT_2: 4, XREAL_1: 29, XXREAL_2:def 1, A3;

          hence thesis by XXREAL_0: 2;

        end;

        take (s - 1);

        let n be Nat;

        s < (s + 1) by XREAL_1: 29;

        then

         A4: (s - 1) < s by XREAL_1: 19;

        

         A5: n in NAT by ORDINAL1:def 12;

        (seq . n) >= s by A1, FUNCT_2: 4, XXREAL_2:def 2, A5;

        hence thesis by A4, XXREAL_0: 2;

      end;

      given t such that

       A6: for n be Nat holds (seq . n) < t;

      given s such that

       A7: for n be Nat holds (seq . n) > s;

      thus ( rng seq) is bounded_below

      proof

        take s;

        let r be ExtReal;

        assume r in ( rng seq);

        then ex n be object st n in ( dom seq) & (seq . n) = r by FUNCT_1:def 3;

        hence thesis by A7;

      end;

      take t;

      let r be ExtReal;

      assume r in ( rng seq);

      then ex n be object st n in ( dom seq) & (seq . n) = r by FUNCT_1:def 3;

      hence thesis by A6;

    end;

    notation

      let X be real-membered set;

      synonym X is with_max for X is right_end;

      synonym X is with_min for X is left_end;

    end

    definition

      let X be real-membered set;

      :: original: with_max

      redefine

      :: MEASURE6:def4

      attr X is with_max means X is bounded_above & ( upper_bound X) in X;

      compatibility

      proof

        thus X is with_max implies X is bounded_above & ( upper_bound X) in X

        proof

          assume

           A1: X is with_max;

          hence X is bounded_above;

          reconsider X as non empty bounded_above real-membered set by A1;

          ( upper_bound X) in X by A1;

          hence thesis;

        end;

        assume

         A2: X is bounded_above & ( upper_bound X) in X;

        then

        reconsider X as non empty bounded_above real-membered set;

        ( upper_bound X) in X by A2;

        hence thesis;

      end;

      :: original: with_min

      redefine

      :: MEASURE6:def5

      attr X is with_min means X is bounded_below & ( lower_bound X) in X;

      compatibility

      proof

        thus X is with_min implies X is bounded_below & ( lower_bound X) in X

        proof

          assume

           A3: X is with_min;

          hence X is bounded_below;

          reconsider X as non empty bounded_below real-membered set by A3;

          ( lower_bound X) in X by A3;

          hence thesis;

        end;

        assume

         A4: X is bounded_below & ( lower_bound X) in X;

        then

        reconsider X as non empty bounded_below real-membered set;

        ( lower_bound X) in X by A4;

        hence thesis;

      end;

    end

    registration

      cluster non empty closed real-bounded for Subset of REAL ;

      existence

      proof

         [. 0 , 0 .] = { 0 } by XXREAL_1: 17;

        hence thesis;

      end;

    end

    definition

      let R be Subset-Family of REAL ;

      :: MEASURE6:def6

      attr R is open means for X be Subset of REAL st X in R holds X is open;

      :: MEASURE6:def7

      attr R is closed means for X be Subset of REAL st X in R holds X is closed;

    end

    reserve r3,r1,q3,p3 for Real;

    definition

      let X be Subset of REAL ;

      :: original: --

      redefine

      func -- X -> Subset of REAL ;

      coherence by MEMBERED: 3;

    end

    theorem :: MEASURE6:40

    r in X iff ( - r) in ( -- X) by MEMBER_1: 11;

    

     Lm2: for X be Subset of REAL st X is bounded_above holds ( -- X) is bounded_below

    proof

      let X be Subset of REAL ;

      given s such that

       A1: s is UpperBound of X;

      take ( - s);

      let t be ExtReal;

      assume t in ( -- X);

      then

      consider r3 be Complex such that

       A2: t = ( - r3) and

       A3: r3 in X;

      reconsider r3 as Real by A3;

      r3 <= s by A1, A3, XXREAL_2:def 1;

      hence thesis by A2, XREAL_1: 24;

    end;

    

     Lm3: for X be Subset of REAL st X is bounded_below holds ( -- X) is bounded_above

    proof

      let X be Subset of REAL ;

      given s such that

       A1: s is LowerBound of X;

      take ( - s);

      let t be ExtReal;

      assume t in ( -- X);

      then

      consider r3 be Complex such that

       A2: t = ( - r3) and

       A3: r3 in X;

      reconsider r3 as Real by A3;

      r3 >= s by A1, A3, XXREAL_2:def 2;

      hence thesis by A2, XREAL_1: 24;

    end;

    theorem :: MEASURE6:41

    

     Th41: X is bounded_above iff ( -- X) is bounded_below

    proof

      X = ( -- ( -- X));

      hence thesis by Lm2, Lm3;

    end;

    theorem :: MEASURE6:42

    X is bounded_below iff ( -- X) is bounded_above

    proof

      X = ( -- ( -- X));

      hence thesis by Th41;

    end;

    theorem :: MEASURE6:43

    

     Th43: for X be non empty Subset of REAL st X is bounded_below holds ( lower_bound X) = ( - ( upper_bound ( -- X)))

    proof

      let X be non empty Subset of REAL ;

      set r = ( - ( upper_bound ( -- X)));

       A1:

      now

        let t;

        assume

         A2: for s st s in X holds s >= t;

        now

          let s;

          assume s in ( -- X);

          then ( - s) in ( -- ( -- X));

          then ( - s) >= t by A2;

          then ( - ( - s)) <= ( - t) by XREAL_1: 24;

          hence s <= ( - t);

        end;

        then ( - r) <= ( - t) by SEQ_4: 45;

        hence r >= t by XREAL_1: 24;

      end;

      assume X is bounded_below;

      then

       A3: ( -- X) is bounded_above by Lm3;

      now

        let s;

        assume s in X;

        then ( - s) in ( -- X);

        then ( - s) <= ( - r) by A3, SEQ_4:def 1;

        hence s >= r by XREAL_1: 24;

      end;

      hence thesis by A1, SEQ_4: 44;

    end;

    theorem :: MEASURE6:44

    

     Th44: for X be non empty Subset of REAL st X is bounded_above holds ( upper_bound X) = ( - ( lower_bound ( -- X)))

    proof

      let X be non empty Subset of REAL ;

      set r = ( - ( lower_bound ( -- X)));

       A1:

      now

        let s;

        assume

         A2: for t st t in X holds t <= s;

        now

          let t;

          assume t in ( -- X);

          then ( - t) in ( -- ( -- X));

          then ( - t) <= s by A2;

          then ( - ( - t)) >= ( - s) by XREAL_1: 24;

          hence t >= ( - s);

        end;

        then ( - r) >= ( - s) by SEQ_4: 43;

        hence r <= s by XREAL_1: 24;

      end;

      assume X is bounded_above;

      then

       A3: ( -- X) is bounded_below by Lm2;

      now

        let t;

        assume t in X;

        then ( - t) in ( -- X);

        then ( - t) >= ( - r) by A3, SEQ_4:def 2;

        hence t <= r by XREAL_1: 24;

      end;

      hence thesis by A1, SEQ_4: 46;

    end;

    

     Lm4: for X be Subset of REAL st X is closed holds ( -- X) is closed

    proof

      let X be Subset of REAL ;

      assume

       A1: X is closed;

      let s1 be Real_Sequence;

      assume that

       A2: ( rng s1) c= ( -- X) and

       A3: s1 is convergent;

      

       A4: ( - ( lim s1)) = ( lim ( - s1)) by A3, SEQ_2: 10;

      

       A5: ( rng ( - s1)) c= X

      proof

        let x be object;

        assume x in ( rng ( - s1));

        then

        consider n be object such that

         A6: n in ( dom ( - s1)) and

         A7: x = (( - s1) . n) by FUNCT_1:def 3;

        reconsider n as Element of NAT by A6;

        

         A8: (s1 . n) in ( rng s1) by FUNCT_2: 4;

        x = ( - (s1 . n)) by A7, SEQ_1: 10;

        then x in ( -- ( -- X)) by A2, A8;

        hence thesis;

      end;

      ( - s1) is convergent by A3;

      then ( lim ( - s1)) in X by A1, A5;

      then ( - ( - ( lim s1))) in ( -- X) by A4;

      hence thesis;

    end;

    theorem :: MEASURE6:45

    X is closed iff ( -- X) is closed

    proof

      ( -- ( -- X)) = X;

      hence thesis by Lm4;

    end;

    

     Lm5: for X be Subset of REAL , p be Real holds (p ++ X) = { (p + r3) : r3 in X }

    proof

      let X be Subset of REAL , p be Real;

      thus (p ++ X) c= { (p + r3) : r3 in X }

      proof

        let x be object;

        assume

         A1: x in (p ++ X);

        then

        reconsider x9 = x as Real;

        ex z be Real st z in X & x9 = (p + z) by A1, Lm1;

        hence thesis;

      end;

      let x be object;

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

      then ex r3 be Real st x = (p + r3) & r3 in X;

      hence thesis by Lm1;

    end;

    theorem :: MEASURE6:46

    

     Th46: r in X iff (q3 + r) in (q3 ++ X)

    proof

      thus r in X implies (q3 + r) in (q3 ++ X) by MEMBER_1: 141;

      assume (q3 + r) in (q3 ++ X);

      then (q3 + r) in { (q3 + r3) : r3 in X } by Lm5;

      then ex mr be Real st (q3 + r) = (q3 + mr) & mr in X;

      hence thesis;

    end;

    theorem :: MEASURE6:47

    X = ( 0 ++ X) by MEMBER_1: 146;

    theorem :: MEASURE6:48

    (q3 ++ (p3 ++ X)) = ((q3 + p3) ++ X) by MEMBER_1: 147;

    

     Lm6: for X be Subset of REAL , s be Real st X is bounded_above holds (s ++ X) is bounded_above

    proof

      let X be Subset of REAL , p be Real;

      given s such that

       A1: s is UpperBound of X;

      take (p + s);

      let t be ExtReal;

      assume t in (p ++ X);

      then t in { (p + r3) : r3 in X } by Lm5;

      then

      consider r3 such that

       A2: t = (p + r3) and

       A3: r3 in X;

      r3 <= s by A1, A3, XXREAL_2:def 1;

      hence thesis by A2, XREAL_1: 6;

    end;

    theorem :: MEASURE6:49

    X is bounded_above iff (q3 ++ X) is bounded_above

    proof

      (( - q3) ++ (q3 ++ X)) = ((( - q3) + q3) ++ X) by MEMBER_1: 147

      .= X by MEMBER_1: 146;

      hence thesis by Lm6;

    end;

    

     Lm7: for X be Subset of REAL , p be Real st X is bounded_below holds (p ++ X) is bounded_below

    proof

      let X be Subset of REAL , p be Real;

      given s such that

       A1: s is LowerBound of X;

      take (p + s);

      let t be ExtReal;

      assume t in (p ++ X);

      then t in { (p + r3) : r3 in X } by Lm5;

      then

      consider r3 such that

       A2: t = (p + r3) and

       A3: r3 in X;

      r3 >= s by A1, A3, XXREAL_2:def 2;

      hence thesis by A2, XREAL_1: 6;

    end;

    theorem :: MEASURE6:50

    X is bounded_below iff (q3 ++ X) is bounded_below

    proof

      (( - q3) ++ (q3 ++ X)) = ((( - q3) + q3) ++ X) by MEMBER_1: 147

      .= X by MEMBER_1: 146;

      hence thesis by Lm7;

    end;

    theorem :: MEASURE6:51

    for X be non empty Subset of REAL st X is bounded_below holds ( lower_bound (q3 ++ X)) = (q3 + ( lower_bound X))

    proof

      let X be non empty Subset of REAL such that

       A1: X is bounded_below;

      set i = (q3 + ( lower_bound X));

       A2:

      now

        let t;

        assume

         A3: for s st s in (q3 ++ X) holds s >= t;

        now

          let s;

          assume s in X;

          then t <= (q3 + s) by A3, MEMBER_1: 141;

          hence (t - q3) <= s by XREAL_1: 20;

        end;

        then ( lower_bound X) >= (t - q3) by SEQ_4: 43;

        hence t <= i by XREAL_1: 20;

      end;

      now

        let s;

        assume s in (q3 ++ X);

        then s in { (q3 + r3) : r3 in X } by Lm5;

        then

        consider r3 such that

         A4: (q3 + r3) = s and

         A5: r3 in X;

        r3 >= ( lower_bound X) by A1, A5, SEQ_4:def 2;

        hence s >= i by A4, XREAL_1: 6;

      end;

      hence thesis by A2, SEQ_4: 44;

    end;

    theorem :: MEASURE6:52

    for X be non empty Subset of REAL st X is bounded_above holds ( upper_bound (q3 ++ X)) = (q3 + ( upper_bound X))

    proof

      let X be non empty Subset of REAL such that

       A1: X is bounded_above;

      set i = (q3 + ( upper_bound X));

       A2:

      now

        let t;

        assume

         A3: for s st s in (q3 ++ X) holds s <= t;

        now

          let s;

          assume s in X;

          then (q3 + s) <= t by A3, MEMBER_1: 141;

          hence s <= (t - q3) by XREAL_1: 19;

        end;

        then ( upper_bound X) <= (t - q3) by SEQ_4: 45;

        hence i <= t by XREAL_1: 19;

      end;

      now

        let s;

        assume s in (q3 ++ X);

        then s in { (q3 + r3) : r3 in X } by Lm5;

        then

        consider r3 such that

         A4: (q3 + r3) = s and

         A5: r3 in X;

        r3 <= ( upper_bound X) by A1, A5, SEQ_4:def 1;

        hence s <= i by A4, XREAL_1: 6;

      end;

      hence thesis by A2, SEQ_4: 46;

    end;

    

     Lm8: for X be Subset of REAL st X is closed holds (q3 ++ X) is closed

    proof

      let X be Subset of REAL ;

      assume

       A1: X is closed;

      

       A2: (q3 ++ X) = { (q3 + r3) : r3 in X } by Lm5;

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

      set s0 = ( seq_const q3);

      let s1 be Real_Sequence;

      assume that

       A3: ( rng s1) c= (q3 ++ X) and

       A4: s1 is convergent;

      ( lim (s1 - s0)) = (( lim s1) - (s0 . 0 )) by A4, SEQ_4: 42

      .= (( lim s1) - q3) by SEQ_1: 57;

      then

       A5: (q3 + ( lim (s1 - s0))) = ( lim s1);

      

       A6: ( rng (s1 - s0)) c= X

      proof

        let x be object;

        assume

         A7: x in ( rng (s1 - s0));

        then

        consider n be object such that

         A8: n in ( dom (s1 - s0)) and

         A9: x = ((s1 - s0) . n) by FUNCT_1:def 3;

        reconsider x9 = x as Real by A7;

        reconsider n as Element of NAT by A8;

        

         A10: (s1 . n) in ( rng s1) by FUNCT_2: 4;

        x = ((s1 . n) + (( - s0) . n)) by A9, SEQ_1: 7

        .= ((s1 . n) + ( - (s0 . n))) by SEQ_1: 10

        .= ((s1 . n) - q3) by SEQ_1: 57;

        then (x9 + q3) in (q3 ++ X) by A3, A10;

        hence thesis by Th46;

      end;

      (s1 - s0) is convergent by A4;

      then ( lim (s1 - s0)) in X by A1, A6;

      hence thesis by A5, A2;

    end;

    theorem :: MEASURE6:53

    X is closed iff (q3 ++ X) is closed

    proof

      (( - q3) ++ (q3 ++ X)) = ((( - q3) + q3) ++ X) by MEMBER_1: 147

      .= X by MEMBER_1: 146;

      hence thesis by Lm8;

    end;

    definition

      let X be Subset of REAL ;

      :: MEASURE6:def8

      func Inv X -> Subset of REAL equals { (1 / r3) : r3 in X };

      coherence

      proof

        set Y = { (1 / r3) : r3 in X };

        Y c= REAL

        proof

          let e be object;

          assume e in Y;

          then ex r3 st e = (1 / r3) & r3 in X;

          hence thesis by XREAL_0:def 1;

        end;

        hence thesis;

      end;

      involutiveness

      proof

        let Y,X be Subset of REAL ;

        assume

         A1: Y = { (1 / r3) : r3 in X };

        thus X c= { (1 / r3) : r3 in Y }

        proof

          let e be object;

          assume

           A2: e in X;

          then

          reconsider r = e as Element of REAL ;

          

           A3: (1 / (1 / r)) = r;

          (1 / r) in Y by A1, A2;

          hence thesis by A3;

        end;

        let e be object;

        assume e in { (1 / r3) : r3 in Y };

        then

        consider r3 such that

         A4: e = (1 / r3) and

         A5: r3 in Y;

        ex r1 st r3 = (1 / r1) & r1 in X by A1, A5;

        hence thesis by A4;

      end;

    end

    theorem :: MEASURE6:54

    

     Th54: for X be Subset of REAL holds r in X iff (1 / r) in ( Inv X)

    proof

      let X be Subset of REAL ;

      thus r in X implies (1 / r) in ( Inv X);

      assume (1 / r) in ( Inv X);

      then ex mr be Real st (1 / r) = (1 / mr) & mr in X;

      hence thesis by XCMPLX_1: 59;

    end;

    registration

      let X be non empty Subset of REAL ;

      cluster ( Inv X) -> non empty;

      coherence

      proof

        ex x be Element of REAL st x in X by SUBSET_1: 4;

        hence thesis by Th54;

      end;

    end

    registration

      let X be without_zero Subset of REAL ;

      cluster ( Inv X) -> without_zero;

      coherence

      proof

        now

          assume 0 in ( Inv X);

          then ex r3 st 0 = (1 / r3) & r3 in X;

          hence contradiction;

        end;

        hence thesis;

      end;

    end

    theorem :: MEASURE6:55

    for X be without_zero Subset of REAL st X is closed real-bounded holds ( Inv X) is closed

    proof

      let X be without_zero Subset of REAL ;

      assume that

       A1: X is closed and

       A2: X is real-bounded;

      let s1 be Real_Sequence;

      assume that

       A3: ( rng s1) c= ( Inv X) and

       A4: s1 is convergent;

      

       A5: ( rng (s1 " )) c= X

      proof

        let x be object;

        assume x in ( rng (s1 " ));

        then

        consider n be object such that

         A6: n in ( dom (s1 " )) and

         A7: x = ((s1 " ) . n) by FUNCT_1:def 3;

        reconsider n as Element of NAT by A6;

        (s1 . n) in ( rng s1) by FUNCT_2: 4;

        then (1 / (s1 . n)) in ( Inv ( Inv X)) by A3;

        hence thesis by A7, VALUED_1: 10;

      end;

      

       A8: not 0 in ( rng s1) by A3;

       A9:

      now

        assume not s1 is non-zero;

        then

        consider n be Nat such that

         A10: (s1 . n) = 0 by SEQ_1: 5;

        n in NAT by ORDINAL1:def 12;

        hence contradiction by A8, FUNCT_2: 4, A10;

      end;

       A11:

      now

        

         A12: ( rng (s1 " )) c= X

        proof

          let y be object;

          assume y in ( rng (s1 " ));

          then

          consider x be object such that

           A13: x in ( dom (s1 " )) and

           A14: y = ((s1 " ) . x) by FUNCT_1:def 3;

          reconsider x as Element of NAT by A13;

          (s1 . x) in ( rng s1) by FUNCT_2: 4;

          then (1 / (s1 . x)) in ( Inv ( Inv X)) by A3;

          hence thesis by A14, VALUED_1: 10;

        end;

        assume ( lim s1) = 0 ;

        then (s1 " ) is non bounded by A4, A9, Th38;

        then ( rng (s1 " )) is non real-bounded by Th39;

        hence contradiction by A2, A12, XXREAL_2: 45;

      end;

      then (s1 " ) is convergent by A4, A9, SEQ_2: 21;

      then ( lim (s1 " )) in X by A1, A5;

      then (1 / ( lim s1)) in X by A4, A9, A11, SEQ_2: 22;

      then (1 / (1 / ( lim s1))) in ( Inv X);

      hence thesis;

    end;

    theorem :: MEASURE6:56

    

     Th56: for Z be Subset-Family of REAL st Z is closed holds ( meet Z) is closed

    proof

      let Z be Subset-Family of REAL ;

      assume

       A1: Z is closed;

      let seq be Real_Sequence;

      set mZ = ( meet Z);

      assume that

       A2: ( rng seq) c= mZ and

       A3: seq is convergent;

      per cases ;

        suppose Z = {} ;

        then mZ = {} by SETFAM_1:def 1;

        hence thesis by A2;

      end;

        suppose

         A4: Z <> {} ;

        now

          let X be set;

          assume

           A5: X in Z;

          then

          reconsider X9 = X as Subset of REAL ;

          

           A6: ( rng seq) c= X by A2, A5, SETFAM_1:def 1;

          X9 is closed by A1, A5;

          hence ( lim seq) in X by A3, A6;

        end;

        hence thesis by A4, SETFAM_1:def 1;

      end;

    end;

    definition

      let X be real-membered set;

      :: MEASURE6:def9

      func Cl X -> Subset of REAL equals ( meet { A where A be Subset of REAL : X c= A & A is closed });

      coherence

      proof

        defpred P[ Subset of REAL ] means X c= $1 & $1 is closed;

        reconsider Z = { A where A be Subset of REAL : P[A] } as Subset-Family of REAL from DOMAIN_1:sch 7;

        reconsider Z as Subset-Family of REAL ;

        ( meet Z) is Subset of REAL ;

        hence thesis;

      end;

      projectivity

      proof

        reconsider W = ( [#] REAL ) as Subset of REAL ;

        let IT be Subset of REAL , X be real-membered set;

        set ClX = { A where A be Subset of REAL : X c= A & A is closed }, ClIT = { A where A be Subset of REAL : IT c= A & A is closed };

        assume

         A1: IT = ( meet ClX);

        X c= W by MEMBERED: 3;

        then

         A2: W in ClX;

        

         A3: W in ClIT;

        thus IT c= ( meet { A where A be Subset of REAL : IT c= A & A is closed })

        proof

          let e be object;

          assume

           A4: e in IT;

          for Y be set holds Y in ClIT implies e in Y

          proof

            let Y be set;

            assume Y in ClIT;

            then

            consider A be Subset of REAL such that

             A5: A = Y and

             A6: IT c= A and

             A7: A is closed;

            for Z be set st Z in ClX holds X c= Z

            proof

              let Z be set;

              assume Z in ClX;

              then ex B be Subset of REAL st Z = B & X c= B & B is closed;

              hence thesis;

            end;

            then X c= IT by A1, A2, SETFAM_1: 5;

            then X c= A by A6;

            then A in ClX by A7;

            hence thesis by A1, A4, A5, SETFAM_1:def 1;

          end;

          hence thesis by A3, SETFAM_1:def 1;

        end;

        let e be object;

        assume

         A8: e in ( meet ClIT);

        for Y be set holds Y in ClX implies e in Y

        proof

          let Y be set;

          assume

           A9: Y in ClX;

          then

          consider A be Subset of REAL such that

           A10: A = Y and X c= A and

           A11: A is closed;

          IT c= A by A1, A9, A10, SETFAM_1: 3;

          then A in ClIT by A11;

          hence thesis by A8, A10, SETFAM_1:def 1;

        end;

        hence thesis by A1, A2, SETFAM_1:def 1;

      end;

    end

    registration

      let X be real-membered set;

      cluster ( Cl X) -> closed;

      coherence

      proof

        defpred P[ Subset of REAL ] means X c= $1 & $1 is closed;

        reconsider Z = { A where A be Subset of REAL : P[A] } as Subset-Family of REAL from DOMAIN_1:sch 7;

        reconsider Z as Subset-Family of REAL ;

        Z is closed

        proof

          let Y be Subset of REAL ;

          assume Y in Z;

          then ex A be Subset of REAL st Y = A & X c= A & A is closed;

          hence thesis;

        end;

        hence thesis by Th56;

      end;

    end

    theorem :: MEASURE6:57

    

     Th57: for Y be closed Subset of REAL st X c= Y holds ( Cl X) c= Y

    proof

      let Y be closed Subset of REAL ;

      set ClX = { A where A be Subset of REAL : X c= A & A is closed };

      assume X c= Y;

      then Y in ClX;

      hence thesis by SETFAM_1: 3;

    end;

    theorem :: MEASURE6:58

    

     Th58: for X be real-membered set holds X c= ( Cl X)

    proof

      let X be real-membered set;

      let x be object;

      set ClX = { A where A be Subset of REAL : X c= A & A is closed };

      assume

       A1: x in X;

       A2:

      now

        let Y be set;

        assume Y in ClX;

        then ex YY be Subset of REAL st YY = Y & X c= YY & YY is closed;

        hence x in Y by A1;

      end;

      X c= ( [#] REAL ) by MEMBERED: 3;

      then ( [#] REAL ) in ClX;

      hence thesis by A2, SETFAM_1:def 1;

    end;

    theorem :: MEASURE6:59

    

     Th59: X is closed iff X = ( Cl X)

    proof

      hereby

        set ClX = { A where A be Subset of REAL : X c= A & A is closed };

        assume X is closed;

        then X in ClX;

        then

         A1: ( Cl X) c= X by SETFAM_1: 3;

        X c= ( Cl X) by Th58;

        hence X = ( Cl X) by A1;

      end;

      thus thesis;

    end;

    theorem :: MEASURE6:60

    ( Cl ( {} REAL )) = {} by Th59;

    theorem :: MEASURE6:61

    ( Cl ( [#] REAL )) = REAL by Th59;

    theorem :: MEASURE6:62

    for X,Y be real-membered set holds X c= Y implies ( Cl X) c= ( Cl Y)

    proof

      let X,Y be real-membered set;

      assume

       A1: X c= Y;

      set ClX = { A where A be Subset of REAL : X c= A & A is closed };

      Y c= ( Cl Y) by Th58;

      then X c= ( Cl Y) by A1;

      then ( Cl Y) in ClX;

      hence thesis by SETFAM_1: 3;

    end;

    theorem :: MEASURE6:63

    

     Th63: r3 in ( Cl X) iff for O be open Subset of REAL st r3 in O holds (O /\ X) is non empty

    proof

      hereby

        assume

         A1: r3 in ( Cl X);

        let O be open Subset of REAL such that

         A2: r3 in O and

         A3: (O /\ X) is empty;

        O misses X by A3;

        then

         A4: X c= (O ` ) by SUBSET_1: 23;

        

         A5: O misses (O ` ) by SUBSET_1: 24;

        (O ` ) is closed by RCOMP_1:def 5;

        then ( Cl X) c= (O ` ) by A4, Th57;

        hence contradiction by A1, A2, A5, XBOOLE_0: 3;

      end;

      

       A6: (( Cl X) ` ) is open;

      X c= ( Cl X) & ((( Cl X) ` ) /\ X) c= X by Th58, XBOOLE_1: 17;

      then

       A7: ((( Cl X) ` ) /\ X) c= ( Cl X);

      ((( Cl X) ` ) /\ X) c= (( Cl X) ` ) by XBOOLE_1: 17;

      then

       A8: ((( Cl X) ` ) /\ X) is empty by A7, SUBSET_1: 20;

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

      assume for O be open Subset of REAL st r3 in O holds (O /\ X) is non empty;

      then not rr3 in (( Cl X) ` ) by A6, A8;

      hence thesis by SUBSET_1: 29;

    end;

    theorem :: MEASURE6:64

    r3 in ( Cl X) implies ex seq st ( rng seq) c= X & seq is convergent & ( lim seq) = r3

    proof

      defpred P[ object, object] means ex n be Nat st $1 = n & $2 = the Element of (X /\ ].(r3 - (1 / (n + 1))), (r3 + (1 / (n + 1))).[);

      assume

       A1: r3 in ( Cl X);

       A2:

      now

        let x be object;

        assume x in NAT ;

        then

        reconsider n = x as Element of NAT ;

        set n1 = (n + 1);

        set oi = ].(r3 - (1 / n1)), (r3 + (1 / n1)).[;

        reconsider u = the Element of (X /\ oi) as object;

        take u;

        

         A3: r3 < (r3 + (1 / n1)) by XREAL_1: 29;

        then (r3 - (1 / n1)) < r3 by XREAL_1: 19;

        then r3 in oi by A3;

        then (X /\ oi) is non empty by A1, Th63;

        then u in (X /\ oi);

        hence u in REAL ;

        thus P[x, u];

      end;

      consider seq be Function such that

       A4: ( dom seq) = NAT & ( rng seq) c= REAL and

       A5: for x be object st x in NAT holds P[x, (seq . x)] from FUNCT_1:sch 6( A2);

      reconsider seq as Real_Sequence by A4, FUNCT_2:def 1, RELSET_1: 4;

      take seq;

      thus ( rng seq) c= X

      proof

        let y be object;

        assume y in ( rng seq);

        then

        consider x be object such that

         A6: x in ( dom seq) and

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

        consider n be Nat such that x = n and

         A8: (seq . x) = the Element of (X /\ ].(r3 - (1 / (n + 1))), (r3 + (1 / (n + 1))).[) by A5, A6;

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

        set n1 = (n + 1);

        set oi = ].(r3 - (1 / n1)), (r3 + (1 / n1)).[;

        

         A9: r3 < (r3 + (1 / n1)) by XREAL_1: 29;

        then (r3 - (1 / n1)) < r3 by XREAL_1: 19;

        then r3 in oi by A9;

        then (X /\ oi) is non empty by A1, Th63;

        hence thesis by A7, A8, XBOOLE_0:def 4;

      end;

       A10:

      now

        let p be Real;

        set cp = [/(1 / p)\];

        

         A11: (1 / p) <= cp by INT_1:def 7;

        assume

         A12: 0 < p;

        then

         A13: 0 < cp by INT_1:def 7;

        then

        reconsider cp as Element of NAT by INT_1: 3;

        reconsider n = cp as Nat;

        take n;

        n < (n + 1) by NAT_1: 13;

        then

         A14: (1 / (n + 1)) < (1 / n) by A13, XREAL_1: 88;

        (1 / (1 / p)) >= (1 / cp) by A12, A11, XREAL_1: 85;

        then

         A15: (1 / (n + 1)) < p by A14, XXREAL_0: 2;

        let m be Nat;

        assume n <= m;

        then

         A16: (n + 1) <= (m + 1) by XREAL_1: 6;

        set m1 = (m + 1);

        (1 / m1) <= (1 / (n + 1)) by A16, XREAL_1: 85;

        then

         A17: (1 / m1) < p by A15, XXREAL_0: 2;

        set oi = ].(r3 - (1 / m1)), (r3 + (1 / m1)).[;

        

         A18: r3 < (r3 + (1 / m1)) by XREAL_1: 29;

        then (r3 - (1 / m1)) < r3 by XREAL_1: 19;

        then r3 in oi by A18;

        then

         A19: (X /\ oi) is non empty by A1, Th63;

        m in NAT by ORDINAL1:def 12;

        then ex m9 be Nat st m9 = m & (seq . m) = the Element of (X /\ ].(r3 - (1 / (m9 + 1))), (r3 + (1 / (m9 + 1))).[) by A5;

        then (seq . m) in oi by A19, XBOOLE_0:def 4;

        then

        consider s such that

         A20: (seq . m) = s and

         A21: (r3 - (1 / m1)) < s & s < (r3 + (1 / m1));

        ( - (1 / m1)) < (s - r3) & (s - r3) < (1 / m1) by A21, XREAL_1: 19, XREAL_1: 20;

        then |.(s - r3).| < (1 / m1) by SEQ_2: 1;

        hence |.((seq . m) - r3).| < p by A20, A17, XXREAL_0: 2;

      end;

      hence seq is convergent;

      hence thesis by A10, SEQ_2:def 7;

    end;

    begin

    definition

      let X be set, f be Function of X, REAL ;

      :: original: bounded_below

      redefine

      :: MEASURE6:def10

      attr f is bounded_below means (f .: X) is bounded_below;

      compatibility

      proof

        

         A1: ( dom f) = X by FUNCT_2:def 1;

        thus f is bounded_below implies (f .: X) is bounded_below

        proof

          given r such that

           A2: for y be object st y in ( dom f) holds r < (f . y);

          take r;

          let s be ExtReal;

          assume s in (f .: X);

          then ex x be object st x in X & x in X & s = (f . x) by FUNCT_2: 64;

          hence thesis by A1, A2;

        end;

        given p be Real such that

         A3: p is LowerBound of (f .: X);

        take (p - 1);

        let y be object;

        assume y in ( dom f);

        then (f . y) in ( rng f) by FUNCT_1: 3;

        then (f . y) in (f .: X) by RELSET_1: 22;

        then

         A4: p <= (f . y) by A3, XXREAL_2:def 2;

        (f . y) < ((f . y) + 1) by XREAL_1: 29;

        then p < ((f . y) + 1) by A4, XXREAL_0: 2;

        hence thesis by XREAL_1: 19;

      end;

      :: original: bounded_above

      redefine

      :: MEASURE6:def11

      attr f is bounded_above means (f .: X) is bounded_above;

      compatibility

      proof

        

         A5: ( dom f) = X by FUNCT_2:def 1;

        thus f is bounded_above implies (f .: X) is bounded_above

        proof

          given r such that

           A6: for y be object st y in ( dom f) holds r > (f . y);

          take r;

          let s be ExtReal;

          assume s in (f .: X);

          then ex x be object st x in X & x in X & s = (f . x) by FUNCT_2: 64;

          hence thesis by A5, A6;

        end;

        given p be Real such that

         A7: p is UpperBound of (f .: X);

        take (p + 1);

        let y be object;

        assume y in ( dom f);

        then (f . y) in ( rng f) by FUNCT_1: 3;

        then (f . y) in (f .: X) by RELSET_1: 22;

        then p >= (f . y) by A7, XXREAL_2:def 1;

        then

         A8: (p + 1) >= ((f . y) + 1) by XREAL_1: 6;

        (f . y) < ((f . y) + 1) by XREAL_1: 29;

        hence thesis by A8, XXREAL_0: 2;

      end;

    end

    definition

      let X be set, f be Function of X, REAL ;

      :: MEASURE6:def12

      attr f is with_max means (f .: X) is with_max;

      :: MEASURE6:def13

      attr f is with_min means (f .: X) is with_min;

    end

    theorem :: MEASURE6:65

    

     Th65: for X,A be set, f be Function of X, REAL holds (( - f) .: A) = ( -- (f .: A))

    proof

      let X,A be set, f be Function of X, REAL ;

      now

        let x be object;

        hereby

          assume x in (( - f) .: A);

          then

          consider x1 be object such that

           A1: x1 in X & x1 in A & x = (( - f) . x1) by FUNCT_2: 64;

          x = ( - (f . x1)) & (f . x1) in (f .: A) by A1, FUNCT_2: 35, VALUED_1: 8;

          hence x in ( -- (f .: A));

        end;

        assume x in ( -- (f .: A));

        then

        consider r3 be Complex such that

         A2: x = ( - r3) and

         A3: r3 in (f .: A);

        reconsider r3 as Real by A3;

        consider x1 be object such that

         A4: x1 in X & x1 in A and

         A5: r3 = (f . x1) by A3, FUNCT_2: 64;

        x = (( - f) . x1) by A2, A5, VALUED_1: 8;

        hence x in (( - f) .: A) by A4, FUNCT_2: 35;

      end;

      hence thesis by TARSKI: 2;

    end;

    

     Lm9: for X be non empty set, f be Function of X, REAL st f is with_max holds ( - f) is with_min

    proof

      let X be non empty set, f be Function of X, REAL ;

      assume that

       A1: (f .: X) is bounded_above and

       A2: ( upper_bound (f .: X)) in (f .: X);

      

       A3: ( -- (f .: X)) = (( - f) .: X) by Th65;

      hence (( - f) .: X) is bounded_below by A1, Lm2;

      

      then

       A4: ( lower_bound (( - f) .: X)) = ( - ( upper_bound ( -- ( -- (f .: X))))) by A3, Th43

      .= ( - ( upper_bound (f .: X)));

      ( - ( upper_bound (f .: X))) in ( -- (f .: X)) by A2;

      hence thesis by A4, Th65;

    end;

    

     Lm10: for X be non empty set, f be Function of X, REAL st f is with_min holds ( - f) is with_max

    proof

      let X be non empty set, f be Function of X, REAL ;

      assume that

       A1: (f .: X) is bounded_below and

       A2: ( lower_bound (f .: X)) in (f .: X);

      

       A3: ( -- (f .: X)) = (( - f) .: X) by Th65;

      hence (( - f) .: X) is bounded_above by A1, Lm3;

      

      then

       A4: ( upper_bound (( - f) .: X)) = ( - ( lower_bound ( -- ( -- (f .: X))))) by A3, Th44

      .= ( - ( lower_bound (f .: X)));

      ( - ( lower_bound (f .: X))) in ( -- (f .: X)) by A2;

      hence thesis by A4, Th65;

    end;

    theorem :: MEASURE6:66

    

     Th66: for X be non empty set, f be Function of X, REAL holds f is with_min iff ( - f) is with_max

    proof

      let X be non empty set, f be Function of X, REAL ;

      ( - ( - f)) = f;

      hence thesis by Lm9, Lm10;

    end;

    theorem :: MEASURE6:67

    for X be non empty set, f be Function of X, REAL holds f is with_max iff ( - f) is with_min

    proof

      let X be non empty set, f be Function of X, REAL ;

      ( - ( - f)) = f;

      hence thesis by Th66;

    end;

    theorem :: MEASURE6:68

    for X be set, A be Subset of REAL , f be Function of X, REAL holds (( - f) " A) = (f " ( -- A))

    proof

      let X be set, A be Subset of REAL , f be Function of X, REAL ;

      now

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        hereby

          

           A1: (( - f) . x) = ( - (f . xx)) by VALUED_1: 8;

          assume

           A2: x in (( - f) " A);

          then (( - f) . x) in A by FUNCT_2: 38;

          then ( - ( - (f . xx))) in ( -- A) by A1;

          hence x in (f " ( -- A)) by A2, FUNCT_2: 38;

        end;

        

         A3: (( - f) . x) = ( - (f . xx)) by VALUED_1: 8;

        assume

         A4: x in (f " ( -- A));

        then (f . x) in ( -- A) by FUNCT_2: 38;

        then (( - f) . x) in ( -- ( -- A)) by A3;

        hence x in (( - f) " A) by A4, FUNCT_2: 38;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: MEASURE6:69

    for X,A be set, f be Function of X, REAL , s be Real holds ((s + f) .: A) = (s ++ (f .: A))

    proof

      let X,A be set, f be Function of X, REAL , s be Real;

      now

        let x be object;

        hereby

          assume x in ((s + f) .: A);

          then

          consider x1 be object such that

           A1: x1 in X & x1 in A & x = ((s + f) . x1) by FUNCT_2: 64;

          x = (s + (f . x1)) & (f . x1) in (f .: A) by A1, FUNCT_2: 35, VALUED_1: 2;

          then x in { (s + q3) : q3 in (f .: A) };

          hence x in (s ++ (f .: A)) by Lm5;

        end;

        assume x in (s ++ (f .: A));

        then x in { (s + q3) : q3 in (f .: A) } by Lm5;

        then

        consider r3 such that

         A2: x = (s + r3) and

         A3: r3 in (f .: A);

        consider x1 be object such that

         A4: x1 in X and

         A5: x1 in A and

         A6: r3 = (f . x1) by A3, FUNCT_2: 64;

        x = ((s + f) . x1) by A2, A4, A6, VALUED_1: 2;

        hence x in ((s + f) .: A) by A4, A5, FUNCT_2: 35;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: MEASURE6:70

    for X be set, A be Subset of REAL , f be Function of X, REAL , q3 holds ((q3 + f) " A) = (f " (( - q3) ++ A))

    proof

      let X be set, A be Subset of REAL , f be Function of X, REAL , q3 be Real;

      now

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        hereby

          assume

           A1: x in ((q3 + f) " A);

          then ((q3 + f) . x) in A & ((q3 + f) . x) = (q3 + (f . xx)) by FUNCT_2: 38, VALUED_1: 2;

          then (( - q3) + (q3 + (f . xx))) in { (( - q3) + p3) : p3 in A };

          then (( - q3) + (q3 + (f . xx))) in (( - q3) ++ A) by Lm5;

          hence x in (f " (( - q3) ++ A)) by A1, FUNCT_2: 38;

        end;

        assume

         A2: x in (f " (( - q3) ++ A));

        then (f . x) in (( - q3) ++ A) & ((q3 + f) . x) = (q3 + (f . xx)) by FUNCT_2: 38, VALUED_1: 2;

        then ((q3 + f) . x) in { (q3 + p3) : p3 in (( - q3) ++ A) };

        then ((q3 + f) . x) in (q3 ++ (( - q3) ++ A)) by Lm5;

        then ((q3 + f) . x) in ((q3 + ( - q3)) ++ A) by MEMBER_1: 147;

        then ((q3 + f) . x) in A by MEMBER_1: 146;

        hence x in ((q3 + f) " A) by A2, FUNCT_2: 38;

      end;

      hence thesis by TARSKI: 2;

    end;

    notation

      let f be real-valued Function;

      synonym Inv f for f " ;

    end

    definition

      let C be set;

      let D be real-membered set;

      let f be PartFunc of C, D;

      :: original: Inv

      redefine

      func Inv f -> PartFunc of C, REAL ;

      coherence

      proof

        (f " ) is PartFunc of C, REAL ;

        hence thesis;

      end;

    end

    theorem :: MEASURE6:71

    for X be set, A be without_zero Subset of REAL , f be Function of X, REAL holds (( Inv f) " A) = (f " ( Inv A))

    proof

      let X be set, A be without_zero Subset of REAL , f be Function of X, REAL ;

      now

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        hereby

          

           A1: (( Inv f) . x) = ((f . xx) " ) by VALUED_1: 10;

          assume

           A2: x in (( Inv f) " A);

          then (( Inv f) . x) in A by FUNCT_2: 38;

          then (1 / ((f . xx) " )) in ( Inv A) by A1;

          hence x in (f " ( Inv A)) by A2, FUNCT_2: 38;

        end;

        

         A3: ((f . xx) " ) = (1 / (f . xx)) & (( Inv f) . x) = ((f . xx) " ) by VALUED_1: 10;

        assume

         A4: x in (f " ( Inv A));

        then (f . x) in ( Inv A) by FUNCT_2: 38;

        then (( Inv f) . x) in ( Inv ( Inv A)) by A3;

        hence x in (( Inv f) " A) by A4, FUNCT_2: 38;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: MEASURE6:72

    for A be Subset of REAL , x be Real st x in ( -- A) holds ex a be Real st a in A & x = ( - a)

    proof

      let A be Subset of REAL , x be Real;

      assume x in ( -- A);

      then x in { ( - a) where a be Complex : a in A };

      then

      consider a be Complex such that

       A1: x = ( - a) & a in A;

      reconsider a as Real by A1;

      take a;

      thus thesis by A1;

    end;