mesfunc1.miz



    begin

    reserve k for Element of NAT ;

    reserve r,r1 for Real;

    reserve i for Integer;

    reserve q for Rational;

    definition

      :: MESFUNC1:def1

      func INT- -> Subset of REAL means

      : Def1: r in it iff ex k st r = ( - k);

      existence

      proof

        defpred P[ Element of REAL ] means ex k st $1 = ( - k);

        consider IT be Subset of REAL such that

         A1: for r be Element of REAL holds r in IT iff P[r] from SUBSET_1:sch 3;

        take IT;

        let r;

        r in REAL by XREAL_0:def 1;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let D1,D2 be Subset of REAL such that

         A2: r in D1 iff ex k st r = ( - k) and

         A3: r in D2 iff ex k st r = ( - k);

        for r be Element of REAL holds r in D1 iff r in D2

        proof

          let r be Element of REAL ;

          thus r in D1 implies r in D2

          proof

            assume r in D1;

            then ex k st r = ( - k) by A2;

            hence thesis by A3;

          end;

          assume r in D2;

          then ex k st r = ( - k) by A3;

          hence thesis by A2;

        end;

        hence thesis by SUBSET_1: 3;

      end;

      correctness ;

    end

    

     Lm1: 0 = ( - 0 );

    registration

      cluster INT- -> non empty;

      coherence by Def1, Lm1;

    end

    theorem :: MESFUNC1:1

    

     Th1: ( NAT , INT- ) are_equipotent

    proof

      defpred P[ Element of NAT , set] means $2 = ( - $1);

      

       A1: for x be Element of NAT holds ex y be Element of INT- st P[x, y]

      proof

        let x be Element of NAT ;

        ( - x) in INT- by Def1;

        hence thesis;

      end;

      consider f be sequence of INT- such that

       A2: for x be Element of NAT holds P[x, (f . x)] from FUNCT_2:sch 3( A1);

      

       A3: f in ( Funcs ( NAT , INT- )) by FUNCT_2: 8;

      then

       A4: ( dom f) = NAT by FUNCT_2: 92;

      

       A5: for x1,x2 be object st x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2) holds x1 = x2

      proof

        let x1,x2 be object;

        assume that

         A6: x1 in ( dom f) and

         A7: x2 in ( dom f) and

         A8: (f . x1) = (f . x2);

        reconsider x1 as Element of NAT by A3, A6, FUNCT_2: 92;

        reconsider x2 as Element of NAT by A3, A7, FUNCT_2: 92;

        (f . x1) = ( - x1) & (f . x2) = ( - x2) by A2;

        then ( - ( - x1)) = x2 by A8;

        hence thesis;

      end;

      

       A9: for y be object st y in INT- holds (f " {y}) <> {}

      proof

        let y be object;

        assume

         A10: y in INT- ;

        then

        reconsider y as Real;

        consider k be Element of NAT such that

         A11: y = ( - k) by A10, Def1;

        (f . k) = ( - k) by A2;

        then (f . k) in {y} by A11, TARSKI:def 1;

        hence thesis by A4, FUNCT_1:def 7;

      end;

      

       A12: f is one-to-one by A5, FUNCT_1:def 4;

      ( rng f) = INT- by A9, FUNCT_2: 41;

      hence thesis by A4, A12, WELLORD2:def 4;

    end;

    theorem :: MESFUNC1:2

    

     Th2: INT = ( INT- \/ NAT )

    proof

      for x be object st x in INT holds x in ( INT- \/ NAT )

      proof

        let x be object;

        assume x in INT ;

        then

        consider k be Nat such that

         A1: x = k or x = ( - k) by INT_1:def 1;

        

         A2: k in NAT by ORDINAL1:def 12;

        per cases by A1;

          suppose x = k;

          hence thesis by XBOOLE_0:def 3, A2;

        end;

          suppose x = ( - k);

          then x in INT- by Def1, A2;

          hence thesis by XBOOLE_0:def 3;

        end;

      end;

      then

       A3: INT c= ( INT- \/ NAT );

      for x be object st x in ( INT- \/ NAT ) holds x in INT

      proof

        let x be object;

        assume

         A4: x in ( INT- \/ NAT );

        now

          per cases by A4, XBOOLE_0:def 3;

            suppose x in INT- ;

            then ex k be Element of NAT st x = ( - k) by Def1;

            hence thesis by INT_1:def 1;

          end;

            suppose x in NAT ;

            hence thesis by INT_1:def 1;

          end;

        end;

        hence thesis;

      end;

      then ( INT- \/ NAT ) c= INT ;

      hence thesis by A3, XBOOLE_0:def 10;

    end;

    theorem :: MESFUNC1:3

    

     Th3: ( NAT , INT ) are_equipotent by Th1, Th2, CARD_2: 77;

    definition

      let n be Nat;

      :: MESFUNC1:def2

      func RAT_with_denominator n -> Subset of RAT means

      : Def2: q in it iff ex i st q = (i / n);

      existence

      proof

        defpred P[ Element of RAT ] means ex i st $1 = (i / n);

        consider X be Subset of RAT such that

         A1: for r be Element of RAT holds r in X iff P[r] from SUBSET_1:sch 3;

        

         A2: for q be Rational holds q in X iff ex i st q = (i / n)

        proof

          let q be Rational;

          reconsider q as Element of RAT by RAT_1:def 2;

          q in X iff ex i st q = (i / n) by A1;

          hence thesis;

        end;

        take X;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let D1,D2 be Subset of RAT such that

         A3: q in D1 iff ex i st q = (i / n) and

         A4: q in D2 iff ex i st q = (i / n);

        for q be Element of RAT holds q in D1 iff q in D2

        proof

          let q be Element of RAT ;

          thus q in D1 implies q in D2

          proof

            assume

             A5: q in D1;

            reconsider q as Rational;

            ex i st q = (i / n) by A3, A5;

            hence thesis by A4;

          end;

          assume

           A6: q in D2;

          reconsider q as Rational;

          ex i st q = (i / n) by A4, A6;

          hence thesis by A3;

        end;

        hence thesis by SUBSET_1: 3;

      end;

    end

    registration

      let n be Nat;

      cluster ( RAT_with_denominator (n + 1)) -> non empty;

      coherence

      proof

        reconsider i1 = (n + 1) as Integer;

        reconsider q = ( 0 / i1) as Rational;

        q in ( RAT_with_denominator (n + 1)) by Def2;

        hence thesis;

      end;

    end

    theorem :: MESFUNC1:4

    

     Th4: for n be Nat holds ( INT ,( RAT_with_denominator (n + 1))) are_equipotent

    proof

      let n be Nat;

      defpred P[ Element of INT , set] means $2 = ($1 / (n + 1));

      

       A1: for x be Element of INT holds ex y be Element of ( RAT_with_denominator (n + 1)) st P[x, y]

      proof

        let x be Element of INT ;

        reconsider x as Integer;

        reconsider i1 = (n + 1) as Integer;

        set y = (x / i1);

        y in RAT by RAT_1:def 1;

        then

        reconsider y as Rational;

        y in ( RAT_with_denominator (n + 1)) by Def2;

        hence thesis;

      end;

      consider f be Function of INT , ( RAT_with_denominator (n + 1)) such that

       A2: for x be Element of INT holds P[x, (f . x)] from FUNCT_2:sch 3( A1);

      

       A3: f in ( Funcs ( INT ,( RAT_with_denominator (n + 1)))) by FUNCT_2: 8;

      then

       A4: ( dom f) = INT by FUNCT_2: 92;

      

       A5: for x1,x2 be object st x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2) holds x1 = x2

      proof

        let x1,x2 be object;

        assume that

         A6: x1 in ( dom f) and

         A7: x2 in ( dom f) and

         A8: (f . x1) = (f . x2);

        reconsider x1 as Element of INT by A3, A6, FUNCT_2: 92;

        reconsider x2 as Element of INT by A3, A7, FUNCT_2: 92;

        (f . x1) = (x1 / (n + 1)) & (f . x2) = (x2 / (n + 1)) by A2;

        hence thesis by A8, XCMPLX_1: 53;

      end;

      

       A9: for y be object st y in ( RAT_with_denominator (n + 1)) holds (f " {y}) <> {}

      proof

        let y be object;

        assume

         A10: y in ( RAT_with_denominator (n + 1));

        then

        reconsider y as Rational;

        consider i be Integer such that

         A11: y = (i / (n + 1)) by A10, Def2;

        reconsider i as Element of INT by INT_1:def 2;

        (f . i) = (i / (n + 1)) by A2;

        then (f . i) in {y} by A11, TARSKI:def 1;

        hence thesis by A4, FUNCT_1:def 7;

      end;

      

       A12: f is one-to-one by A5, FUNCT_1:def 4;

      ( rng f) = ( RAT_with_denominator (n + 1)) by A9, FUNCT_2: 41;

      hence thesis by A4, A12, WELLORD2:def 4;

    end;

    theorem :: MESFUNC1:5

    ( NAT , RAT ) are_equipotent

    proof

      assume

       A1: not ( NAT , RAT ) are_equipotent ;

      defpred P[ Element of NAT , Subset of REAL ] means $2 = ( RAT_with_denominator ($1 + 1));

      

       A2: for n be Element of NAT holds ex X be Subset of REAL st P[n, X]

      proof

        let n be Element of NAT ;

        for x be object st x in ( RAT_with_denominator (n + 1)) holds x in REAL by NUMBERS: 12;

        then

        reconsider X = ( RAT_with_denominator (n + 1)) as Subset of REAL by TARSKI:def 3;

        take X;

        thus thesis;

      end;

      consider F be sequence of ( bool REAL ) such that

       A3: for n be Element of NAT holds P[n, (F . n)] from FUNCT_2:sch 3( A2);

      for x be object st x in ( union ( rng F)) holds x in RAT

      proof

        let x be object;

        assume x in ( union ( rng F));

        then

        consider Y be set such that

         A4: x in Y and

         A5: Y in ( rng F) by TARSKI:def 4;

        ( dom F) = NAT by FUNCT_2:def 1;

        then

        consider n be object such that

         A6: n in NAT and

         A7: (F . n) = Y by A5, FUNCT_1:def 3;

        reconsider n as Element of NAT by A6;

        Y = ( RAT_with_denominator (n + 1)) by A3, A7;

        hence thesis by A4;

      end;

      then

       A8: ( union ( rng F)) c= RAT ;

      for x be object st x in RAT holds x in ( union ( rng F))

      proof

        let x be object;

        assume x in RAT ;

        then

        reconsider x as Rational;

        

         A9: ( dom F) = NAT by FUNCT_2:def 1;

        ( denominator x) <> 0 by RAT_1:def 3;

        then

        consider m be Nat such that

         A10: ( denominator x) = (m + 1) by NAT_1: 6;

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

        ( denominator x) = (m + 1) by A10;

        then

        reconsider n = (( denominator x) - 1) as Element of NAT ;

        x = (( numerator x) / (n + 1)) by RAT_1: 15;

        then x in ( RAT_with_denominator (n + 1)) by Def2;

        then

         A11: x in (F . n) by A3;

        (F . n) in ( rng F) by A9, FUNCT_1:def 3;

        hence thesis by A11, TARSKI:def 4;

      end;

      then RAT c= ( union ( rng F));

      then

       A12: ( union ( rng F)) = RAT by A8, XBOOLE_0:def 10;

      ( dom F) = NAT by FUNCT_2:def 1;

      then

       A13: ( rng F) is countable by CARD_3: 93;

      for Y be set st Y in ( rng F) holds Y is countable

      proof

        let Y be set;

        assume Y in ( rng F);

        then

        consider n be object such that

         A14: n in ( dom F) and

         A15: (F . n) = Y by FUNCT_1:def 3;

        reconsider n as Element of NAT by A14, FUNCT_2:def 1;

        Y = ( RAT_with_denominator (n + 1)) by A3, A15;

        then ( INT ,Y) are_equipotent by Th4;

        then ( NAT ,Y) are_equipotent by Th3, WELLORD2: 15;

        then

         A16: ( card NAT ) = ( card Y) by CARD_1: 5;

        thus thesis by A16, CARD_3:def 14;

      end;

      then RAT is countable by A12, A13, CARD_4: 12;

      then ( card RAT ) c= omega by CARD_3:def 14;

      then not omega in ( card RAT );

      then not omega c= ( card RAT ) or not omega <> ( card RAT ) by CARD_1: 3;

      then ( card RAT ) in omega by A1, CARD_1: 4, CARD_1: 5, CARD_1: 47;

      hence contradiction;

    end;

    begin

    definition

      let C be non empty set;

      let f1,f2 be C -defined ExtREAL -valued Function;

      deffunc F( Element of C) = ((f1 . $1) + (f2 . $1));

      :: MESFUNC1:def3

      func f1 + f2 -> PartFunc of C, ExtREAL means ( dom it ) = ((( dom f1) /\ ( dom f2)) \ (((f1 " { -infty }) /\ (f2 " { +infty })) \/ ((f1 " { +infty }) /\ (f2 " { -infty })))) & for c be Element of C st c in ( dom it ) holds (it . c) = ((f1 . c) + (f2 . c));

      existence

      proof

        defpred P[ Element of C] means $1 in ((( dom f1) /\ ( dom f2)) \ (((f1 " { -infty }) /\ (f2 " { +infty })) \/ ((f1 " { +infty }) /\ (f2 " { -infty }))));

        consider F be PartFunc of C, ExtREAL such that

         A1: for c be Element of C holds c in ( dom F) iff P[c] and

         A2: for c be Element of C st c in ( dom F) holds (F . c) = F(c) from SEQ_1:sch 3;

        take F;

        for x be object st x in ( dom F) holds x in ((( dom f1) /\ ( dom f2)) \ (((f1 " { -infty }) /\ (f2 " { +infty })) \/ ((f1 " { +infty }) /\ (f2 " { -infty }))))

        proof

          let x be object;

          assume

           A3: x in ( dom F);

          ( dom F) c= C by RELAT_1:def 18;

          then

          reconsider x as Element of C by A3;

          x in ( dom F) by A3;

          hence thesis by A1;

        end;

        then

         A4: ( dom F) c= ((( dom f1) /\ ( dom f2)) \ (((f1 " { -infty }) /\ (f2 " { +infty })) \/ ((f1 " { +infty }) /\ (f2 " { -infty }))));

        for x be object st x in ((( dom f1) /\ ( dom f2)) \ (((f1 " { -infty }) /\ (f2 " { +infty })) \/ ((f1 " { +infty }) /\ (f2 " { -infty })))) holds x in ( dom F)

        proof

          let x be object;

          assume

           A5: x in ((( dom f1) /\ ( dom f2)) \ (((f1 " { -infty }) /\ (f2 " { +infty })) \/ ((f1 " { +infty }) /\ (f2 " { -infty }))));

          then

           A6: x in ( dom f1) by XBOOLE_0:def 4;

          ( dom f1) c= C by RELAT_1:def 18;

          then

          reconsider x as Element of C by A6;

          x in ((( dom f1) /\ ( dom f2)) \ (((f1 " { -infty }) /\ (f2 " { +infty })) \/ ((f1 " { +infty }) /\ (f2 " { -infty })))) by A5;

          hence thesis by A1;

        end;

        then ((( dom f1) /\ ( dom f2)) \ (((f1 " { -infty }) /\ (f2 " { +infty })) \/ ((f1 " { +infty }) /\ (f2 " { -infty })))) c= ( dom F);

        hence ( dom F) = ((( dom f1) /\ ( dom f2)) \ (((f1 " { -infty }) /\ (f2 " { +infty })) \/ ((f1 " { +infty }) /\ (f2 " { -infty })))) by A4, XBOOLE_0:def 10;

        let c be Element of C;

        assume c in ( dom F);

        hence thesis by A2;

      end;

      uniqueness

      proof

        set X = ((( dom f1) /\ ( dom f2)) \ (((f1 " { -infty }) /\ (f2 " { +infty })) \/ ((f1 " { +infty }) /\ (f2 " { -infty }))));

        thus for f,g be PartFunc of C, ExtREAL st (( dom f) = X & for c be Element of C st c in ( dom f) holds (f . c) = F(c)) & (( dom g) = X & for c be Element of C st c in ( dom g) holds (g . c) = F(c)) holds f = g from SEQ_1:sch 4;

      end;

      commutativity ;

      deffunc F( Element of C) = ((f1 . $1) - (f2 . $1));

      :: MESFUNC1:def4

      func f1 - f2 -> PartFunc of C, ExtREAL means ( dom it ) = ((( dom f1) /\ ( dom f2)) \ (((f1 " { +infty }) /\ (f2 " { +infty })) \/ ((f1 " { -infty }) /\ (f2 " { -infty })))) & for c be Element of C st c in ( dom it ) holds (it . c) = ((f1 . c) - (f2 . c));

      existence

      proof

        defpred P[ Element of C] means $1 in ((( dom f1) /\ ( dom f2)) \ (((f1 " { +infty }) /\ (f2 " { +infty })) \/ ((f1 " { -infty }) /\ (f2 " { -infty }))));

        consider F be PartFunc of C, ExtREAL such that

         A7: for c be Element of C holds c in ( dom F) iff P[c] and

         A8: for c be Element of C st c in ( dom F) holds (F . c) = F(c) from SEQ_1:sch 3;

        take F;

        for x be object st x in ( dom F) holds x in ((( dom f1) /\ ( dom f2)) \ (((f1 " { +infty }) /\ (f2 " { +infty })) \/ ((f1 " { -infty }) /\ (f2 " { -infty }))))

        proof

          let x be object;

          assume

           A9: x in ( dom F);

          ( dom F) c= C by RELAT_1:def 18;

          then

          reconsider x as Element of C by A9;

          x in ( dom F) by A9;

          hence thesis by A7;

        end;

        then

         A10: ( dom F) c= ((( dom f1) /\ ( dom f2)) \ (((f1 " { +infty }) /\ (f2 " { +infty })) \/ ((f1 " { -infty }) /\ (f2 " { -infty }))));

        for x be object st x in ((( dom f1) /\ ( dom f2)) \ (((f1 " { +infty }) /\ (f2 " { +infty })) \/ ((f1 " { -infty }) /\ (f2 " { -infty })))) holds x in ( dom F)

        proof

          let x be object;

          assume

           A11: x in ((( dom f1) /\ ( dom f2)) \ (((f1 " { +infty }) /\ (f2 " { +infty })) \/ ((f1 " { -infty }) /\ (f2 " { -infty }))));

          then

           A12: x in ( dom f1) by XBOOLE_0:def 4;

          ( dom f1) c= C by RELAT_1:def 18;

          then

          reconsider x as Element of C by A12;

          x in ((( dom f1) /\ ( dom f2)) \ (((f1 " { +infty }) /\ (f2 " { +infty })) \/ ((f1 " { -infty }) /\ (f2 " { -infty })))) by A11;

          hence thesis by A7;

        end;

        then ((( dom f1) /\ ( dom f2)) \ (((f1 " { +infty }) /\ (f2 " { +infty })) \/ ((f1 " { -infty }) /\ (f2 " { -infty })))) c= ( dom F);

        hence ( dom F) = ((( dom f1) /\ ( dom f2)) \ (((f1 " { +infty }) /\ (f2 " { +infty })) \/ ((f1 " { -infty }) /\ (f2 " { -infty })))) by A10, XBOOLE_0:def 10;

        let c be Element of C;

        assume c in ( dom F);

        hence thesis by A8;

      end;

      uniqueness

      proof

        set X = ((( dom f1) /\ ( dom f2)) \ (((f1 " { +infty }) /\ (f2 " { +infty })) \/ ((f1 " { -infty }) /\ (f2 " { -infty }))));

        thus for f,g be PartFunc of C, ExtREAL st (( dom f) = X & for c be Element of C st c in ( dom f) holds (f . c) = F(c)) & (( dom g) = X & for c be Element of C st c in ( dom g) holds (g . c) = F(c)) holds f = g from SEQ_1:sch 4;

      end;

      deffunc F( Element of C) = ((f1 . $1) * (f2 . $1));

      :: MESFUNC1:def5

      func f1 (#) f2 -> PartFunc of C, ExtREAL means ( dom it ) = (( dom f1) /\ ( dom f2)) & for c be Element of C st c in ( dom it ) holds (it . c) = ((f1 . c) * (f2 . c));

      existence

      proof

        defpred P[ Element of C] means $1 in (( dom f1) /\ ( dom f2));

        consider F be PartFunc of C, ExtREAL such that

         A13: for c be Element of C holds c in ( dom F) iff P[c] and

         A14: for c be Element of C st c in ( dom F) holds (F . c) = F(c) from SEQ_1:sch 3;

        take F;

        for x be object st x in ( dom F) holds x in (( dom f1) /\ ( dom f2))

        proof

          let x be object;

          assume

           A15: x in ( dom F);

          ( dom F) c= C by RELAT_1:def 18;

          then

          reconsider x as Element of C by A15;

          x in ( dom F) by A15;

          hence thesis by A13;

        end;

        then

         A16: ( dom F) c= (( dom f1) /\ ( dom f2));

        for x be object st x in (( dom f1) /\ ( dom f2)) holds x in ( dom F)

        proof

          let x be object;

          assume

           A17: x in (( dom f1) /\ ( dom f2));

          then

           A18: x in ( dom f1) by XBOOLE_0:def 4;

          ( dom f1) c= C by RELAT_1:def 18;

          then

          reconsider x as Element of C by A18;

          x in (( dom f1) /\ ( dom f2)) by A17;

          hence thesis by A13;

        end;

        then (( dom f1) /\ ( dom f2)) c= ( dom F);

        hence ( dom F) = (( dom f1) /\ ( dom f2)) by A16, XBOOLE_0:def 10;

        let c be Element of C;

        assume c in ( dom F);

        hence thesis by A14;

      end;

      uniqueness

      proof

        set X = (( dom f1) /\ ( dom f2));

        thus for F,G be PartFunc of C, ExtREAL st (( dom F) = X & for c be Element of C st c in ( dom F) holds (F . c) = F(c)) & (( dom G) = X & for c be Element of C st c in ( dom G) holds (G . c) = F(c)) holds F = G from SEQ_1:sch 4;

      end;

      commutativity ;

    end

    definition

      let C be non empty set, f be C -defined ExtREAL -valued Function, r be Real;

      deffunc F( Element of C) = ( In ((r * (f . $1)), ExtREAL ));

      :: MESFUNC1:def6

      func r (#) f -> PartFunc of C, ExtREAL means

      : Def6: ( dom it ) = ( dom f) & for c be Element of C st c in ( dom it ) holds (it . c) = (r * (f . c));

      existence

      proof

        defpred P[ Element of C] means $1 in ( dom f);

        consider F be PartFunc of C, ExtREAL such that

         A1: for c be Element of C holds c in ( dom F) iff P[c] and

         A2: for c be Element of C st c in ( dom F) holds (F . c) = F(c) from SEQ_1:sch 3;

        take F;

        for x be object st x in ( dom F) holds x in ( dom f)

        proof

          let x be object;

          assume

           A3: x in ( dom F);

          ( dom F) c= C by RELAT_1:def 18;

          then

          reconsider x as Element of C by A3;

          x in ( dom F) by A3;

          hence thesis by A1;

        end;

        then

         A4: ( dom F) c= ( dom f);

        for x be object st x in ( dom f) holds x in ( dom F)

        proof

          let x be object;

          assume

           A5: x in ( dom f);

          ( dom f) c= C by RELAT_1:def 18;

          then

          reconsider x as Element of C by A5;

          x in ( dom f) by A5;

          hence thesis by A1;

        end;

        then ( dom f) c= ( dom F);

        hence ( dom F) = ( dom f) by A4, XBOOLE_0:def 10;

        let c be Element of C;

        assume c in ( dom F);

        then (F . c) = F(c) by A2;

        hence thesis;

      end;

      uniqueness

      proof

        set X = ( dom f);

        deffunc F( Element of C) = (r * (f . $1));

        thus for F,G be PartFunc of C, ExtREAL st (( dom F) = X & for c be Element of C st c in ( dom F) holds (F . c) = F(c)) & (( dom G) = X & for c be Element of C st c in ( dom G) holds (G . c) = F(c)) holds F = G from SEQ_1:sch 4;

      end;

    end

    theorem :: MESFUNC1:6

    

     Th6: for C be non empty set, f be PartFunc of C, ExtREAL , r st r <> 0 holds for c be Element of C st c in ( dom (r (#) f)) holds (f . c) = (((r (#) f) . c) / r)

    proof

      let C be non empty set;

      let f be PartFunc of C, ExtREAL ;

      let r;

      assume

       A1: r <> 0 ;

      let c be Element of C;

      assume c in ( dom (r (#) f));

      then

       A2: ((r (#) f) . c) = (r * (f . c)) by Def6;

      per cases ;

        suppose

         A3: (f . c) = +infty ;

        now

          per cases by A1;

            suppose

             A4: 0. < r;

            then ((r (#) f) . c) = +infty by A2, A3, XXREAL_3:def 5;

            hence thesis by A3, A4, XXREAL_3: 83;

          end;

            suppose

             A5: r < 0. ;

            then ((r (#) f) . c) = -infty by A2, A3, XXREAL_3:def 5;

            hence thesis by A3, A5, XXREAL_3: 84;

          end;

        end;

        hence thesis;

      end;

        suppose

         A6: (f . c) = -infty ;

        now

          per cases by A1;

            suppose

             A7: 0. < r;

            then ((r (#) f) . c) = -infty by A2, A6, XXREAL_3:def 5;

            hence thesis by A6, A7, XXREAL_3: 86;

          end;

            suppose

             A8: r < 0. ;

            then ((r (#) f) . c) = +infty by A2, A6, XXREAL_3:def 5;

            hence thesis by A6, A8, XXREAL_3: 85;

          end;

        end;

        hence thesis;

      end;

        suppose (f . c) <> +infty & (f . c) <> -infty ;

        then

        reconsider a = (f . c) as Element of REAL by XXREAL_0: 14;

        reconsider rr = r as R_eal by XXREAL_0:def 1;

        ((r (#) f) . c) = (r qua ExtReal * a) by A2

        .= (r * a);

        

        then (((r (#) f) . c) / rr) = ((r * a) / r)

        .= (a / (r / r)) by XCMPLX_1: 77

        .= (a / 1) by A1, XCMPLX_1: 60;

        hence thesis;

      end;

    end;

    definition

      let C be non empty set;

      let f be C -defined ExtREAL -valued Function;

      deffunc F( Element of C) = ( - (f . $1));

      :: MESFUNC1:def7

      func - f -> PartFunc of C, ExtREAL means ( dom it ) = ( dom f) & for c be Element of C st c in ( dom it ) holds (it . c) = ( - (f . c));

      existence

      proof

        defpred P[ Element of C] means $1 in ( dom f);

        consider F be PartFunc of C, ExtREAL such that

         A1: for c be Element of C holds c in ( dom F) iff P[c] and

         A2: for c be Element of C st c in ( dom F) holds (F . c) = F(c) from SEQ_1:sch 3;

        take F;

        for x be object st x in ( dom F) holds x in ( dom f)

        proof

          let x be object;

          assume

           A3: x in ( dom F);

          ( dom F) c= C by RELAT_1:def 18;

          then

          reconsider x as Element of C by A3;

          x in ( dom F) by A3;

          hence thesis by A1;

        end;

        then

         A4: ( dom F) c= ( dom f);

        for x be object st x in ( dom f) holds x in ( dom F)

        proof

          let x be object;

          assume

           A5: x in ( dom f);

          ( dom f) c= C by RELAT_1:def 18;

          then

          reconsider x as Element of C by A5;

          x in ( dom f) by A5;

          hence thesis by A1;

        end;

        then ( dom f) c= ( dom F);

        hence ( dom F) = ( dom f) by A4, XBOOLE_0:def 10;

        let c be Element of C;

        assume c in ( dom F);

        hence thesis by A2;

      end;

      uniqueness

      proof

        set X = ( dom f);

        thus for F,G be PartFunc of C, ExtREAL st (( dom F) = X & for c be Element of C st c in ( dom F) holds (F . c) = F(c)) & (( dom G) = X & for c be Element of C st c in ( dom G) holds (G . c) = F(c)) holds F = G from SEQ_1:sch 4;

      end;

    end

    ::$Canceled

    definition

      let C be non empty set;

      let f be C -defined ExtREAL -valued Function;

      let r be Real;

      deffunc F( Element of C) = ( In ((r / (f . $1)), ExtREAL ));

      :: MESFUNC1:def8

      func r / f -> PartFunc of C, ExtREAL means

      : Def9: ( dom it ) = (( dom f) \ (f " { 0. })) & for c be Element of C st c in ( dom it ) holds (it . c) = (r / (f . c));

      existence

      proof

        defpred P[ Element of C] means $1 in (( dom f) \ (f " { 0. }));

        consider F be PartFunc of C, ExtREAL such that

         A1: for c be Element of C holds c in ( dom F) iff P[c] and

         A2: for c be Element of C st c in ( dom F) holds (F . c) = F(c) from SEQ_1:sch 3;

        take F;

        for x be object st x in ( dom F) holds x in (( dom f) \ (f " { 0. }))

        proof

          let x be object;

          assume

           A3: x in ( dom F);

          ( dom F) c= C by RELAT_1:def 18;

          then

          reconsider x as Element of C by A3;

          x in ( dom F) by A3;

          hence thesis by A1;

        end;

        then

         A4: ( dom F) c= (( dom f) \ (f " { 0. }));

        for x be object st x in (( dom f) \ (f " { 0. })) holds x in ( dom F)

        proof

          let x be object;

          assume

           A5: x in (( dom f) \ (f " { 0. }));

          ( dom f) c= C by RELAT_1:def 18;

          then (( dom f) \ (f " { 0. })) c= C;

          then

          reconsider x as Element of C by A5;

          x in (( dom f) \ (f " { 0. })) by A5;

          hence thesis by A1;

        end;

        then (( dom f) \ (f " { 0. })) c= ( dom F);

        hence ( dom F) = (( dom f) \ (f " { 0. })) by A4, XBOOLE_0:def 10;

        let c be Element of C;

        assume c in ( dom F);

        then (F . c) = F(c) by A2;

        hence thesis;

      end;

      uniqueness

      proof

        set X = (( dom f) \ (f " { 0. }));

        deffunc F( Element of C) = (r / (f . $1));

        thus for F,G be PartFunc of C, ExtREAL st (( dom F) = X & for c be Element of C st c in ( dom F) holds (F . c) = F(c)) & (( dom G) = X & for c be Element of C st c in ( dom G) holds (G . c) = F(c)) holds F = G from SEQ_1:sch 4;

      end;

    end

    theorem :: MESFUNC1:7

    for C be non empty set, f be PartFunc of C, ExtREAL holds ( dom (1 / f)) = (( dom f) \ (f " { 0. })) & for c be Element of C st c in ( dom (1 / f)) holds ((1 / f) . c) = ( 1. / (f . c)) by Def9;

    definition

      let C be non empty set;

      let f be C -defined ExtREAL -valued Function;

      deffunc F( Element of C) = |.(f . $1).|;

      :: MESFUNC1:def9

      func |.f.| -> PartFunc of C, ExtREAL means ( dom it ) = ( dom f) & for c be Element of C st c in ( dom it ) holds (it . c) = |.(f . c).|;

      existence

      proof

        defpred P[ Element of C] means $1 in ( dom f);

        consider F be PartFunc of C, ExtREAL such that

         A1: for c be Element of C holds c in ( dom F) iff P[c] and

         A2: for c be Element of C st c in ( dom F) holds (F . c) = F(c) from SEQ_1:sch 3;

        take F;

        for x be object st x in ( dom F) holds x in ( dom f)

        proof

          let x be object;

          assume

           A3: x in ( dom F);

          ( dom F) c= C by RELAT_1:def 18;

          then

          reconsider x as Element of C by A3;

          x in ( dom F) by A3;

          hence thesis by A1;

        end;

        then

         A4: ( dom F) c= ( dom f);

        for x be object st x in ( dom f) holds x in ( dom F)

        proof

          let x be object;

          assume

           A5: x in ( dom f);

          ( dom f) c= C by RELAT_1:def 18;

          then

          reconsider x as Element of C by A5;

          x in ( dom f) by A5;

          hence thesis by A1;

        end;

        then ( dom f) c= ( dom F);

        hence ( dom F) = ( dom f) by A4, XBOOLE_0:def 10;

        let c be Element of C;

        assume c in ( dom F);

        hence thesis by A2;

      end;

      uniqueness

      proof

        set X = ( dom f);

        thus for F,G be PartFunc of C, ExtREAL st (( dom F) = X & for c be Element of C st c in ( dom F) holds (F . c) = F(c)) & (( dom G) = X & for c be Element of C st c in ( dom G) holds (G . c) = F(c)) holds F = G from SEQ_1:sch 4;

      end;

    end

    begin

    theorem :: MESFUNC1:8

    

     Th8: ex n be Element of NAT st r <= n

    proof

      per cases ;

        suppose [/r\] >= 0 ;

        then

        reconsider n = [/r\] as Element of NAT by INT_1: 3;

        take n;

        thus thesis by INT_1:def 7;

      end;

        suppose

         A1: [/r\] < 0 ;

        take 0 ;

        thus thesis by A1, INT_1:def 7;

      end;

    end;

    theorem :: MESFUNC1:9

    

     Th9: ex n be Nat st ( - n) <= r

    proof

       [\r/] is Element of INT by INT_1:def 2;

      then

       A1: [\r/] <= r & ex k be Nat st ( [\r/] = k or [\r/] = ( - k)) by INT_1:def 1, INT_1:def 6;

      per cases ;

        suppose [\r/] < 0 ;

        hence thesis by A1;

      end;

        suppose

         A2: [\r/] >= 0 ;

        take 0 ;

        thus thesis by A2, INT_1:def 6;

      end;

    end;

    theorem :: MESFUNC1:10

    

     Th10: for r,s be Real st r < s holds ex n be Element of NAT st (1 / (n + 1)) < (s - r)

    proof

      let r,s be Real;

      assume r < s;

      then (s - r) > 0 by XREAL_1: 50;

      then

      consider t be Real such that

       A1: 0 < t and

       A2: t < (s - r) by XREAL_1: 5;

      reconsider t as Real;

      

       A3: (1 / t) > 0 by A1, XREAL_1: 139;

      

       A4: ( [/(1 / t)\] + 1) > (1 / t) by INT_1: 32;

      set n = [/(1 / t)\];

      reconsider n as Element of NAT by A3, A4, INT_1: 3, INT_1: 7;

      ((n + 1) * t) >= 1 by A1, A4, XREAL_1: 81;

      then (1 / (n + 1)) <= t by XREAL_1: 79;

      then (1 / (n + 1)) < (s - r) by A2, XXREAL_0: 2;

      hence thesis;

    end;

    theorem :: MESFUNC1:11

    

     Th11: for r,s be Real st for n be Element of NAT holds (r - (1 / (n + 1))) <= s holds r <= s

    proof

      let r,s be Real;

      assume

       A1: for n be Element of NAT holds (r - (1 / (n + 1))) <= s;

      assume r > s;

      then

      consider n be Element of NAT such that

       A2: (1 / (n + 1)) < (r - s) by Th10;

      (s + (1 / (n + 1))) < r by A2, XREAL_1: 20;

      then s < (r - (1 / (n + 1))) by XREAL_1: 20;

      hence contradiction by A1;

    end;

    theorem :: MESFUNC1:12

    

     Th12: for a be R_eal st for r be Real holds r < a holds a = +infty

    proof

      let a be R_eal;

      assume

       A1: for r be Real holds r < a;

      assume not a = +infty ;

      then a < +infty by XXREAL_0: 4;

      then

      consider b be R_eal such that

       A2: a < b and b < +infty and

       A3: b in REAL by MEASURE5: 2;

      reconsider b as Real by A3;

      a <= b by A2;

      hence contradiction by A1;

    end;

    theorem :: MESFUNC1:13

    

     Th13: for a be R_eal st for r be Real holds a < r holds a = -infty

    proof

      let a be R_eal;

      assume

       A1: for r be Real holds a < r;

      assume

       A2: not a = -infty ;

       -infty <= a by XXREAL_0: 5;

      then -infty < a by A2, XXREAL_0: 1;

      then

      consider b be R_eal such that -infty < b and

       A3: b < a and

       A4: b in REAL by MEASURE5: 2;

      reconsider b as Real by A4;

      b <= a by A3;

      hence contradiction by A1;

    end;

    reserve X for set;

    reserve f for PartFunc of X, ExtREAL ;

    reserve S for SigmaField of X;

    reserve F for sequence of S;

    reserve A for set;

    reserve a for ExtReal;

    reserve r,s for Real;

    reserve n,m for Element of NAT ;

    notation

      let f be ext-real-valued Function, a be ExtReal;

      synonym eq_dom (f,a) for Coim (f,a);

    end

    definition

      let f be ext-real-valued Function, a be ExtReal;

      defpred P[ object] means $1 in ( dom f) & (f . $1) < a;

      :: MESFUNC1:def10

      func less_dom (f,a) -> set means

      : Def11: for x be object holds x in it iff x in ( dom f) & (f . x) < a;

      existence

      proof

        consider A be set such that

         A1: for x be object holds x in A iff x in ( dom f) & P[x] from XBOOLE_0:sch 1;

        take A;

        thus thesis by A1;

      end;

      uniqueness

      proof

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

      end;

      defpred P[ object] means $1 in ( dom f) & (f . $1) <= a;

      :: MESFUNC1:def11

      func less_eq_dom (f,a) -> set means

      : Def12: for x be object holds x in it iff x in ( dom f) & (f . x) <= a;

      existence

      proof

        consider A be set such that

         A2: for x be object holds x in A iff x in ( dom f) & P[x] from XBOOLE_0:sch 1;

        take A;

        thus thesis by A2;

      end;

      uniqueness

      proof

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

      end;

      defpred P[ object] means $1 in ( dom f) & a < (f . $1);

      :: MESFUNC1:def12

      func great_dom (f,a) -> set means

      : Def13: for x be object holds x in it iff x in ( dom f) & a < (f . x);

      existence

      proof

        consider A be set such that

         A3: for x be object holds x in A iff x in ( dom f) & P[x] from XBOOLE_0:sch 1;

        take A;

        thus thesis by A3;

      end;

      uniqueness

      proof

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

      end;

      defpred P[ object] means $1 in ( dom f) & a <= (f . $1);

      :: MESFUNC1:def13

      func great_eq_dom (f,a) -> set means

      : Def14: for x be object holds x in it iff x in ( dom f) & a <= (f . x);

      existence

      proof

        consider A be set such that

         A4: for x be object holds x in A iff x in ( dom f) & P[x] from XBOOLE_0:sch 1;

        take A;

        thus thesis by A4;

      end;

      uniqueness

      proof

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

      end;

      :: original: eq_dom

      redefine

      :: MESFUNC1:def14

      func eq_dom (f,a) means

      : Def15: for x be set holds x in it iff x in ( dom f) & (f . x) = a;

      compatibility

      proof

        let X be set;

        thus X = ( eq_dom (f,a)) implies for x be set holds x in X iff x in ( dom f) & (f . x) = a

        proof

          assume

           A5: X = ( eq_dom (f,a));

          let x be set;

          thus x in X implies x in ( dom f) & (f . x) = a

          proof

            assume

             A6: x in X;

            hence x in ( dom f) by A5, FUNCT_1:def 7;

            (f . x) in {a} by A5, A6, FUNCT_1:def 7;

            hence thesis by TARSKI:def 1;

          end;

          assume

           A7: x in ( dom f);

          assume (f . x) = a;

          then (f . x) in {a} by TARSKI:def 1;

          hence thesis by A5, A7, FUNCT_1:def 7;

        end;

        assume

         A8: for x be set holds x in X iff x in ( dom f) & (f . x) = a;

        for x be object holds x in X iff x in ( dom f) & (f . x) in {a}

        proof

          let x be object;

          thus x in X implies x in ( dom f) & (f . x) in {a}

          proof

            assume

             A9: x in X;

            hence x in ( dom f) by A8;

            (f . x) = a by A8, A9;

            hence thesis by TARSKI:def 1;

          end;

          assume

           A10: x in ( dom f);

          assume (f . x) in {a};

          then (f . x) = a by TARSKI:def 1;

          hence thesis by A8, A10;

        end;

        hence thesis by FUNCT_1:def 7;

      end;

    end

    definition

      let X be set, f be PartFunc of X, ExtREAL , a be ExtReal;

      :: original: less_dom

      redefine

      func less_dom (f,a) -> Subset of X ;

      coherence

      proof

        ( less_dom (f,a)) c= X

        proof

          let x be object;

          assume x in ( less_dom (f,a));

          then

           A1: x in ( dom f) by Def11;

          ( dom f) c= X by RELAT_1:def 18;

          hence thesis by A1;

        end;

        hence thesis;

      end;

      :: original: less_eq_dom

      redefine

      func less_eq_dom (f,a) -> Subset of X ;

      coherence

      proof

        ( less_eq_dom (f,a)) c= X

        proof

          let x be object;

          assume x in ( less_eq_dom (f,a));

          then

           A2: x in ( dom f) by Def12;

          ( dom f) c= X by RELAT_1:def 18;

          hence thesis by A2;

        end;

        hence thesis;

      end;

      :: original: great_dom

      redefine

      func great_dom (f,a) -> Subset of X ;

      coherence

      proof

        ( great_dom (f,a)) c= X

        proof

          let x be object;

          assume x in ( great_dom (f,a));

          then

           A3: x in ( dom f) by Def13;

          ( dom f) c= X by RELAT_1:def 18;

          hence thesis by A3;

        end;

        hence thesis;

      end;

      :: original: great_eq_dom

      redefine

      func great_eq_dom (f,a) -> Subset of X ;

      coherence

      proof

        ( great_eq_dom (f,a)) c= X

        proof

          let x be object;

          assume x in ( great_eq_dom (f,a));

          then

           A4: x in ( dom f) by Def14;

          ( dom f) c= X by RELAT_1:def 18;

          hence thesis by A4;

        end;

        hence thesis;

      end;

      :: original: eq_dom

      redefine

      func eq_dom (f,a) -> Subset of X ;

      coherence

      proof

        ( Coim (f,a)) is Subset of X;

        hence thesis;

      end;

    end

    theorem :: MESFUNC1:14

    

     Th14: A c= ( dom f) implies (A /\ ( great_eq_dom (f,a))) = (A \ (A /\ ( less_dom (f,a))))

    proof

      assume

       A1: A c= ( dom f);

      ( dom f) c= X by RELAT_1:def 18;

      then

       A2: A c= X by A1;

      for x be object st x in (A /\ ( great_eq_dom (f,a))) holds x in (A \ (A /\ ( less_dom (f,a))))

      proof

        let x be object;

        assume

         A3: x in (A /\ ( great_eq_dom (f,a)));

        then

         A4: x in A by XBOOLE_0:def 4;

        x in ( great_eq_dom (f,a)) by A3, XBOOLE_0:def 4;

        then a <= (f . x) by Def14;

        then not x in ( less_dom (f,a)) by Def11;

        then not x in (A /\ ( less_dom (f,a))) by XBOOLE_0:def 4;

        hence thesis by A4, XBOOLE_0:def 5;

      end;

      then

       A5: (A /\ ( great_eq_dom (f,a))) c= (A \ (A /\ ( less_dom (f,a))));

      for x be object st x in (A \ (A /\ ( less_dom (f,a)))) holds x in (A /\ ( great_eq_dom (f,a)))

      proof

        let x be object;

        assume

         A6: x in (A \ (A /\ ( less_dom (f,a))));

        then

         A7: x in A;

         not x in (A /\ ( less_dom (f,a))) by A6, XBOOLE_0:def 5;

        then

         A8: not x in ( less_dom (f,a)) by A6, XBOOLE_0:def 4;

        reconsider x as Element of X by A2, A7;

        reconsider y = (f . x) as R_eal;

         not y < a by A1, A7, A8, Def11;

        then x in ( great_eq_dom (f,a)) by A1, A7, Def14;

        hence thesis by A6, XBOOLE_0:def 4;

      end;

      then (A \ (A /\ ( less_dom (f,a)))) c= (A /\ ( great_eq_dom (f,a)));

      hence thesis by A5, XBOOLE_0:def 10;

    end;

    theorem :: MESFUNC1:15

    

     Th15: A c= ( dom f) implies (A /\ ( great_dom (f,a))) = (A \ (A /\ ( less_eq_dom (f,a))))

    proof

      assume

       A1: A c= ( dom f);

      ( dom f) c= X by RELAT_1:def 18;

      then

       A2: A c= X by A1;

      for x be object st x in (A /\ ( great_dom (f,a))) holds x in (A \ (A /\ ( less_eq_dom (f,a))))

      proof

        let x be object;

        assume

         A3: x in (A /\ ( great_dom (f,a)));

        then

         A4: x in A by XBOOLE_0:def 4;

        x in ( great_dom (f,a)) by A3, XBOOLE_0:def 4;

        then a < (f . x) by Def13;

        then not x in ( less_eq_dom (f,a)) by Def12;

        then not x in (A /\ ( less_eq_dom (f,a))) by XBOOLE_0:def 4;

        hence thesis by A4, XBOOLE_0:def 5;

      end;

      then

       A5: (A /\ ( great_dom (f,a))) c= (A \ (A /\ ( less_eq_dom (f,a))));

      for x be object st x in (A \ (A /\ ( less_eq_dom (f,a)))) holds x in (A /\ ( great_dom (f,a)))

      proof

        let x be object;

        assume

         A6: x in (A \ (A /\ ( less_eq_dom (f,a))));

        then

         A7: x in A;

         not x in (A /\ ( less_eq_dom (f,a))) by A6, XBOOLE_0:def 5;

        then

         A8: not x in ( less_eq_dom (f,a)) by A6, XBOOLE_0:def 4;

        reconsider x as Element of X by A2, A7;

        reconsider y = (f . x) as R_eal;

         not y <= a by A1, A7, A8, Def12;

        then x in ( great_dom (f,a)) by A1, A7, Def13;

        hence thesis by A6, XBOOLE_0:def 4;

      end;

      then (A \ (A /\ ( less_eq_dom (f,a)))) c= (A /\ ( great_dom (f,a)));

      hence thesis by A5, XBOOLE_0:def 10;

    end;

    theorem :: MESFUNC1:16

    

     Th16: A c= ( dom f) implies (A /\ ( less_eq_dom (f,a))) = (A \ (A /\ ( great_dom (f,a))))

    proof

      assume

       A1: A c= ( dom f);

      ( dom f) c= X by RELAT_1:def 18;

      then

       A2: A c= X by A1;

      

       A3: (A /\ ( less_eq_dom (f,a))) c= (A \ (A /\ ( great_dom (f,a))))

      proof

        let x be object;

        assume

         A4: x in (A /\ ( less_eq_dom (f,a)));

        then

         A5: x in A by XBOOLE_0:def 4;

        x in ( less_eq_dom (f,a)) by A4, XBOOLE_0:def 4;

        then (f . x) <= a by Def12;

        then not x in ( great_dom (f,a)) by Def13;

        then not x in (A /\ ( great_dom (f,a))) by XBOOLE_0:def 4;

        hence thesis by A5, XBOOLE_0:def 5;

      end;

      for x be object st x in (A \ (A /\ ( great_dom (f,a)))) holds x in (A /\ ( less_eq_dom (f,a)))

      proof

        let x be object;

        assume

         A6: x in (A \ (A /\ ( great_dom (f,a))));

        then

         A7: x in A;

         not x in (A /\ ( great_dom (f,a))) by A6, XBOOLE_0:def 5;

        then

         A8: not x in ( great_dom (f,a)) by A6, XBOOLE_0:def 4;

        reconsider x as Element of X by A2, A7;

        reconsider y = (f . x) as R_eal;

         not a < y by A1, A7, A8, Def13;

        then x in ( less_eq_dom (f,a)) by A1, A7, Def12;

        hence thesis by A6, XBOOLE_0:def 4;

      end;

      then (A \ (A /\ ( great_dom (f,a)))) c= (A /\ ( less_eq_dom (f,a)));

      hence thesis by A3, XBOOLE_0:def 10;

    end;

    theorem :: MESFUNC1:17

    

     Th17: A c= ( dom f) implies (A /\ ( less_dom (f,a))) = (A \ (A /\ ( great_eq_dom (f,a))))

    proof

      assume

       A1: A c= ( dom f);

      ( dom f) c= X by RELAT_1:def 18;

      then

       A2: A c= X by A1;

      for x be object st x in (A /\ ( less_dom (f,a))) holds x in (A \ (A /\ ( great_eq_dom (f,a))))

      proof

        let x be object;

        assume

         A3: x in (A /\ ( less_dom (f,a)));

        then

         A4: x in A by XBOOLE_0:def 4;

        x in ( less_dom (f,a)) by A3, XBOOLE_0:def 4;

        then (f . x) < a by Def11;

        then not x in ( great_eq_dom (f,a)) by Def14;

        then not x in (A /\ ( great_eq_dom (f,a))) by XBOOLE_0:def 4;

        hence thesis by A4, XBOOLE_0:def 5;

      end;

      then

       A5: (A /\ ( less_dom (f,a))) c= (A \ (A /\ ( great_eq_dom (f,a))));

      for x be object st x in (A \ (A /\ ( great_eq_dom (f,a)))) holds x in (A /\ ( less_dom (f,a)))

      proof

        let x be object;

        assume

         A6: x in (A \ (A /\ ( great_eq_dom (f,a))));

        then

         A7: x in A;

         not x in (A /\ ( great_eq_dom (f,a))) by A6, XBOOLE_0:def 5;

        then

         A8: not x in ( great_eq_dom (f,a)) by A6, XBOOLE_0:def 4;

        reconsider x as Element of X by A2, A7;

        reconsider y = (f . x) as R_eal;

         not a <= y by A1, A7, A8, Def14;

        then x in ( less_dom (f,a)) by A1, A7, Def11;

        hence thesis by A6, XBOOLE_0:def 4;

      end;

      then (A \ (A /\ ( great_eq_dom (f,a)))) c= (A /\ ( less_dom (f,a)));

      hence thesis by A5, XBOOLE_0:def 10;

    end;

    theorem :: MESFUNC1:18

    (A /\ ( eq_dom (f,a))) = ((A /\ ( great_eq_dom (f,a))) /\ ( less_eq_dom (f,a)))

    proof

      for x be object st x in (A /\ ( eq_dom (f,a))) holds x in ((A /\ ( great_eq_dom (f,a))) /\ ( less_eq_dom (f,a)))

      proof

        let x be object;

        assume

         A1: x in (A /\ ( eq_dom (f,a)));

        then

         A2: x in A by XBOOLE_0:def 4;

        

         A3: x in ( eq_dom (f,a)) by A1, XBOOLE_0:def 4;

        then

         A4: a = (f . x) by Def15;

        reconsider x as Element of X by A1;

        

         A5: x in ( dom f) by A3, Def15;

        then x in ( great_eq_dom (f,a)) by A4, Def14;

        then

         A6: x in (A /\ ( great_eq_dom (f,a))) by A2, XBOOLE_0:def 4;

        x in ( less_eq_dom (f,a)) by A4, A5, Def12;

        hence thesis by A6, XBOOLE_0:def 4;

      end;

      then

       A7: (A /\ ( eq_dom (f,a))) c= ((A /\ ( great_eq_dom (f,a))) /\ ( less_eq_dom (f,a)));

      for x be object st x in ((A /\ ( great_eq_dom (f,a))) /\ ( less_eq_dom (f,a))) holds x in (A /\ ( eq_dom (f,a)))

      proof

        let x be object;

        assume

         A8: x in ((A /\ ( great_eq_dom (f,a))) /\ ( less_eq_dom (f,a)));

        then

         A9: x in (A /\ ( great_eq_dom (f,a))) by XBOOLE_0:def 4;

        

         A10: x in ( less_eq_dom (f,a)) by A8, XBOOLE_0:def 4;

        

         A11: x in A by A9, XBOOLE_0:def 4;

        x in ( great_eq_dom (f,a)) by A9, XBOOLE_0:def 4;

        then

         A12: a <= (f . x) by Def14;

        

         A13: (f . x) <= a by A10, Def12;

        reconsider x as Element of X by A8;

        

         A14: x in ( dom f) by A10, Def12;

        a = (f . x) by A12, A13, XXREAL_0: 1;

        then x in ( eq_dom (f,a)) by A14, Def15;

        hence thesis by A11, XBOOLE_0:def 4;

      end;

      then ((A /\ ( great_eq_dom (f,a))) /\ ( less_eq_dom (f,a))) c= (A /\ ( eq_dom (f,a)));

      hence thesis by A7, XBOOLE_0:def 10;

    end;

    theorem :: MESFUNC1:19

    for X, S, F, f, A, r st for n holds (F . n) = (A /\ ( great_dom (f,(r - (1 / (n + 1)))))) holds (A /\ ( great_eq_dom (f,r))) = ( meet ( rng F))

    proof

      let X, S, F, f, A, r;

      assume

       A1: for n holds (F . n) = (A /\ ( great_dom (f,(r - (1 / (n + 1))))));

      for x be object st x in (A /\ ( great_eq_dom (f,r))) holds x in ( meet ( rng F))

      proof

        let x be object;

        assume

         A2: x in (A /\ ( great_eq_dom (f,r)));

        then

         A3: x in A by XBOOLE_0:def 4;

        

         A4: x in ( great_eq_dom (f,r)) by A2, XBOOLE_0:def 4;

        for Y be set holds Y in ( rng F) implies x in Y

        proof

          let Y be set;

          Y in ( rng F) implies x in Y

          proof

            assume Y in ( rng F);

            then

            consider m be Element of NAT such that m in ( dom F) and

             A5: Y = (F . m) by PARTFUN1: 3;

            

             A6: Y = (A /\ ( great_dom (f,(r - (1 / (m + 1)))))) by A1, A5;

            

             A7: x in ( dom f) by A4, Def14;

            reconsider x as Element of X by A2;

            

             A8: r <= (f . x) by A4, Def14;

            ((m + 1) " ) > 0 ;

            then (1 / (m + 1)) > 0 by XCMPLX_1: 215;

            then r < (r + (1 / (m + 1))) by XREAL_1: 29;

            then (r - (1 / (m + 1))) < r by XREAL_1: 19;

            then (r - (1 / (m + 1))) < (f . x) by A8, XXREAL_0: 2;

            then x in ( great_dom (f,(r - (1 / (m + 1))))) by A7, Def13;

            hence thesis by A3, A6, XBOOLE_0:def 4;

          end;

          hence thesis;

        end;

        hence thesis by SETFAM_1:def 1;

      end;

      then

       A9: (A /\ ( great_eq_dom (f,r))) c= ( meet ( rng F));

      for x be object st x in ( meet ( rng F)) holds x in (A /\ ( great_eq_dom (f,r)))

      proof

        let x be object;

        assume

         A10: x in ( meet ( rng F));

        

         A11: for m holds x in A & x in ( dom f) & (r - (1 / (m + 1))) < (f . x)

        proof

          let m;

          m in NAT ;

          then m in ( dom F) by FUNCT_2:def 1;

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

          then x in (F . m) by A10, SETFAM_1:def 1;

          then

           A12: x in (A /\ ( great_dom (f,(r - (1 / (m + 1)))))) by A1;

          then x in ( great_dom (f,(r - (1 / (m + 1))))) by XBOOLE_0:def 4;

          hence thesis by A12, Def13, XBOOLE_0:def 4;

        end;

        reconsider y = (f . x) as R_eal by XXREAL_0:def 1;

        1 in NAT ;

        then 1 in ( dom F) by FUNCT_2:def 1;

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

        then x in (F . 1) by A10, SETFAM_1:def 1;

        then x in (A /\ ( great_dom (f,(r - (1 / (1 + 1)))))) by A1;

        then

        reconsider x as Element of X;

        r <= y

        proof

          now

            per cases ;

              suppose y = +infty ;

              hence thesis by XXREAL_0: 4;

            end;

              suppose not y = +infty ;

              then

               A13: not +infty <= y by XXREAL_0: 4;

              (r - (1 / (1 + 1))) < y by A11;

              then

              reconsider y1 = y as Element of REAL by A13, XXREAL_0: 48;

              for m holds (r - (1 / (m + 1))) <= y1 by A11;

              hence thesis by Th11;

            end;

          end;

          hence thesis;

        end;

        then x in ( great_eq_dom (f,r)) by A11, Def14;

        hence thesis by A11, XBOOLE_0:def 4;

      end;

      then ( meet ( rng F)) c= (A /\ ( great_eq_dom (f,r)));

      hence thesis by A9, XBOOLE_0:def 10;

    end;

    theorem :: MESFUNC1:20

    

     Th20: for r be Real st for n holds (F . n) = (A /\ ( less_dom (f,(r + (1 / (n + 1)))))) holds (A /\ ( less_eq_dom (f,r))) = ( meet ( rng F))

    proof

      let r be Real;

      assume

       A1: for n holds (F . n) = (A /\ ( less_dom (f,(r + (1 / (n + 1))))));

      for x be object st x in (A /\ ( less_eq_dom (f,r))) holds x in ( meet ( rng F))

      proof

        let x be object;

        assume

         A2: x in (A /\ ( less_eq_dom (f,r)));

        then

         A3: x in A by XBOOLE_0:def 4;

        

         A4: x in ( less_eq_dom (f,r)) by A2, XBOOLE_0:def 4;

        for Y be set holds Y in ( rng F) implies x in Y

        proof

          let Y be set;

          Y in ( rng F) implies x in Y

          proof

            assume Y in ( rng F);

            then

            consider m be Element of NAT such that m in ( dom F) and

             A5: Y = (F . m) by PARTFUN1: 3;

            

             A6: Y = (A /\ ( less_dom (f,(r + (1 / (m + 1)))))) by A1, A5;

            

             A7: x in ( dom f) by A4, Def12;

            reconsider x as Element of X by A2;

            

             A8: (f . x) <= r by A4, Def12;

            ((m + 1) " ) > 0 ;

            then (1 / (m + 1)) > 0 by XCMPLX_1: 215;

            then r < (r + (1 / (m + 1))) by XREAL_1: 29;

            then (f . x) < (r + (1 / (m + 1))) by A8, XXREAL_0: 2;

            then x in ( less_dom (f,(r + (1 / (m + 1))))) by A7, Def11;

            hence thesis by A3, A6, XBOOLE_0:def 4;

          end;

          hence thesis;

        end;

        hence thesis by SETFAM_1:def 1;

      end;

      then

       A9: (A /\ ( less_eq_dom (f,r))) c= ( meet ( rng F));

      for x be object st x in ( meet ( rng F)) holds x in (A /\ ( less_eq_dom (f,r)))

      proof

        let x be object;

        assume

         A10: x in ( meet ( rng F));

        

         A11: for m holds x in A & x in ( dom f) & (f . x) < (r + (1 / (m + 1)))

        proof

          let m;

          m in NAT ;

          then m in ( dom F) by FUNCT_2:def 1;

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

          then x in (F . m) by A10, SETFAM_1:def 1;

          then

           A12: x in (A /\ ( less_dom (f,(r + (1 / (m + 1)))))) by A1;

          then x in ( less_dom (f,(r + (1 / (m + 1))))) by XBOOLE_0:def 4;

          hence thesis by A12, Def11, XBOOLE_0:def 4;

        end;

        reconsider y = (f . x) as R_eal by XXREAL_0:def 1;

        1 in NAT ;

        then 1 in ( dom F) by FUNCT_2:def 1;

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

        then x in (F . 1) by A10, SETFAM_1:def 1;

        then x in (A /\ ( less_dom (f,(r + (1 / (1 + 1)))))) by A1;

        then

        reconsider x as Element of X;

        y <= r

        proof

          now

            per cases ;

              suppose y = -infty ;

              hence thesis by XXREAL_0: 5;

            end;

              suppose not y = -infty ;

              then

               A13: not y <= -infty by XXREAL_0: 6;

              y < (r + (1 / (1 + 1))) by A11;

              then

              reconsider y1 = y as Element of REAL by A13, XXREAL_0: 48;

              for m holds (y1 - (1 / (m + 1))) <= r

              proof

                let m;

                y1 < (r + (1 / (m + 1))) by A11;

                hence thesis by XREAL_1: 20;

              end;

              hence thesis by Th11;

            end;

          end;

          hence thesis;

        end;

        then x in ( less_eq_dom (f,r)) by A11, Def12;

        hence thesis by A11, XBOOLE_0:def 4;

      end;

      then ( meet ( rng F)) c= (A /\ ( less_eq_dom (f,r)));

      hence thesis by A9, XBOOLE_0:def 10;

    end;

    theorem :: MESFUNC1:21

    

     Th21: for r be Real st for n holds (F . n) = (A /\ ( less_eq_dom (f,(r - (1 / (n + 1)))))) holds (A /\ ( less_dom (f,r))) = ( union ( rng F))

    proof

      let r be Real;

      assume

       A1: for n holds (F . n) = (A /\ ( less_eq_dom (f,(r - (1 / (n + 1))))));

      for x be object st x in (A /\ ( less_dom (f,r))) holds x in ( union ( rng F))

      proof

        let x be object;

        assume

         A2: x in (A /\ ( less_dom (f,r)));

        then

         A3: x in A by XBOOLE_0:def 4;

        

         A4: x in ( less_dom (f,r)) by A2, XBOOLE_0:def 4;

        ex Y be set st x in Y & Y in ( rng F)

        proof

          reconsider x as Element of X by A2;

          

           A5: x in ( dom f) by A4, Def11;

          

           A6: (f . x) < r by A4, Def11;

          ex m st (f . x) <= (r - (1 / (m + 1)))

          proof

            per cases ;

              suppose

               A7: (f . x) = -infty ;

              take 1;

              thus thesis by A7, XXREAL_0: 5;

            end;

              suppose not (f . x) = -infty ;

              then not (f . x) <= -infty by XXREAL_0: 6;

              then

              reconsider y1 = (f . x) as Element of REAL by A6, XXREAL_0: 48;

              consider m such that

               A8: (1 / (m + 1)) < (r - y1) by A6, Th10;

              (y1 + (1 / (m + 1))) < r by A8, XREAL_1: 20;

              then (f . x) <= (r - (1 / (m + 1))) by XREAL_1: 20;

              hence thesis;

            end;

          end;

          then

          consider m such that

           A9: (f . x) <= (r - (1 / (m + 1)));

          x in ( less_eq_dom (f,(r - (1 / (m + 1))))) by A5, A9, Def12;

          then

           A10: x in (A /\ ( less_eq_dom (f,(r - (1 / (m + 1)))))) by A3, XBOOLE_0:def 4;

          m in NAT ;

          then

           A11: m in ( dom F) by FUNCT_2:def 1;

          take (F . m);

          thus thesis by A1, A10, A11, FUNCT_1:def 3;

        end;

        hence thesis by TARSKI:def 4;

      end;

      then

       A12: (A /\ ( less_dom (f,r))) c= ( union ( rng F));

      for x be object st x in ( union ( rng F)) holds x in (A /\ ( less_dom (f,r)))

      proof

        let x be object;

        assume x in ( union ( rng F));

        then

        consider Y be set such that

         A13: x in Y and

         A14: Y in ( rng F) by TARSKI:def 4;

        consider m such that m in ( dom F) and

         A15: (F . m) = Y by A14, PARTFUN1: 3;

        

         A16: x in (A /\ ( less_eq_dom (f,(r - (1 / (m + 1)))))) by A1, A13, A15;

        then

         A17: x in A by XBOOLE_0:def 4;

        

         A18: x in ( less_eq_dom (f,(r - (1 / (m + 1))))) by A16, XBOOLE_0:def 4;

        then

         A19: x in ( dom f) by Def12;

        

         A20: (f . x) <= (r - (1 / (m + 1))) by A18, Def12;

        reconsider x as Element of X by A13, A14;

        (f . x) < r

        proof

          now

            r < (r + (1 / (m + 1))) by XREAL_1: 29, XREAL_1: 139;

            then (r - (1 / (m + 1))) < r by XREAL_1: 19;

            hence thesis by A20, XXREAL_0: 2;

          end;

          hence thesis;

        end;

        then x in ( less_dom (f,r)) by A19, Def11;

        hence thesis by A17, XBOOLE_0:def 4;

      end;

      then ( union ( rng F)) c= (A /\ ( less_dom (f,r)));

      hence thesis by A12, XBOOLE_0:def 10;

    end;

    theorem :: MESFUNC1:22

    

     Th22: for X, S, F, f, A, r st for n holds (F . n) = (A /\ ( great_eq_dom (f,(r + (1 / (n + 1)))))) holds (A /\ ( great_dom (f,r))) = ( union ( rng F))

    proof

      let X, S, F, f, A, r;

      assume

       A1: for n holds (F . n) = (A /\ ( great_eq_dom (f,(r + (1 / (n + 1))))));

      for x be object st x in (A /\ ( great_dom (f,r))) holds x in ( union ( rng F))

      proof

        let x be object;

        assume

         A2: x in (A /\ ( great_dom (f,r)));

        then

         A3: x in A by XBOOLE_0:def 4;

        

         A4: x in ( great_dom (f,r)) by A2, XBOOLE_0:def 4;

        ex Y be set st x in Y & Y in ( rng F)

        proof

          reconsider x as Element of X by A2;

          

           A5: x in ( dom f) by A4, Def13;

          

           A6: r < (f . x) by A4, Def13;

          ex m st (r + (1 / (m + 1))) <= (f . x)

          proof

            per cases ;

              suppose

               A7: (f . x) = +infty ;

              take 1;

              thus thesis by A7, XXREAL_0: 4;

            end;

              suppose not (f . x) = +infty ;

              then not +infty <= (f . x) by XXREAL_0: 4;

              then

              reconsider y1 = (f . x) as Element of REAL by A6, XXREAL_0: 48;

              consider m such that

               A8: (1 / (m + 1)) < (y1 - r) by A6, Th10;

              take m;

              thus thesis by A8, XREAL_1: 20;

            end;

          end;

          then

          consider m such that

           A9: (r + (1 / (m + 1))) <= (f . x);

          x in ( great_eq_dom (f,(r + (1 / (m + 1))))) by A5, A9, Def14;

          then

           A10: x in (A /\ ( great_eq_dom (f,(r + (1 / (m + 1)))))) by A3, XBOOLE_0:def 4;

          m in NAT ;

          then

           A11: m in ( dom F) by FUNCT_2:def 1;

          take (F . m);

          thus thesis by A1, A10, A11, FUNCT_1:def 3;

        end;

        hence thesis by TARSKI:def 4;

      end;

      then

       A12: (A /\ ( great_dom (f,r))) c= ( union ( rng F));

      for x be object st x in ( union ( rng F)) holds x in (A /\ ( great_dom (f,r)))

      proof

        let x be object;

        assume x in ( union ( rng F));

        then

        consider Y be set such that

         A13: x in Y and

         A14: Y in ( rng F) by TARSKI:def 4;

        consider m such that m in ( dom F) and

         A15: (F . m) = Y by A14, PARTFUN1: 3;

        

         A16: x in (A /\ ( great_eq_dom (f,(r + (1 / (m + 1)))))) by A1, A13, A15;

        then

         A17: x in A by XBOOLE_0:def 4;

        

         A18: x in ( great_eq_dom (f,(r + (1 / (m + 1))))) by A16, XBOOLE_0:def 4;

        then

         A19: x in ( dom f) by Def14;

        

         A20: (r + (1 / (m + 1))) <= (f . x) by A18, Def14;

        reconsider x as Element of X by A13, A14;

        r < (f . x)

        proof

          now

            r < (r + (1 / (m + 1))) by XREAL_1: 29, XREAL_1: 139;

            hence thesis by A20, XXREAL_0: 2;

          end;

          hence thesis;

        end;

        then x in ( great_dom (f,r)) by A19, Def13;

        hence thesis by A17, XBOOLE_0:def 4;

      end;

      then ( union ( rng F)) c= (A /\ ( great_dom (f,r)));

      hence thesis by A12, XBOOLE_0:def 10;

    end;

    theorem :: MESFUNC1:23

    

     Th23: for X, S, F, f, A st for n holds (F . n) = (A /\ ( great_dom (f,n))) holds (A /\ ( eq_dom (f, +infty ))) = ( meet ( rng F))

    proof

      let X, S, F, f, A;

      assume

       A1: for n holds (F . n) = (A /\ ( great_dom (f,n)));

      for x be object st x in (A /\ ( eq_dom (f, +infty ))) holds x in ( meet ( rng F))

      proof

        let x be object;

        assume

         A2: x in (A /\ ( eq_dom (f, +infty )));

        then

         A3: x in A by XBOOLE_0:def 4;

        

         A4: x in ( eq_dom (f, +infty )) by A2, XBOOLE_0:def 4;

        for Y be set holds Y in ( rng F) implies x in Y

        proof

          let Y be set;

          Y in ( rng F) implies x in Y

          proof

            assume Y in ( rng F);

            then

            consider m be Element of NAT such that m in ( dom F) and

             A5: Y = (F . m) by PARTFUN1: 3;

            

             A6: Y = (A /\ ( great_dom (f,m))) by A1, A5;

            reconsider x as Element of X by A2;

            

             A7: (f . x) = +infty by A4, Def15;

            m in REAL by XREAL_0:def 1;

            then x in ( dom f) & not +infty <= m by A4, Def15, XXREAL_0: 9;

            then x in ( great_dom (f,m)) by A7, Def13;

            hence thesis by A3, A6, XBOOLE_0:def 4;

          end;

          hence thesis;

        end;

        hence thesis by SETFAM_1:def 1;

      end;

      then

       A8: (A /\ ( eq_dom (f, +infty ))) c= ( meet ( rng F));

      for x be object st x in ( meet ( rng F)) holds x in (A /\ ( eq_dom (f, +infty )))

      proof

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        assume

         A9: x in ( meet ( rng F));

        

         A10: for m holds x in A & x in ( dom f) & ex y be R_eal st y = (f . x) & y = +infty

        proof

          let m;

          m in NAT ;

          then m in ( dom F) by FUNCT_2:def 1;

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

          then x in (F . m) by A9, SETFAM_1:def 1;

          then

           A11: x in (A /\ ( great_dom (f,m))) by A1;

          then

           A12: x in ( great_dom (f,m)) by XBOOLE_0:def 4;

          for r holds r < (f . xx)

          proof

            let r;

            consider n such that

             A13: r <= n by Th8;

            n in NAT ;

            then n in ( dom F) by FUNCT_2:def 1;

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

            then x in (F . n) by A9, SETFAM_1:def 1;

            then x in (A /\ ( great_dom (f,n))) by A1;

            then x in ( great_dom (f,n)) by XBOOLE_0:def 4;

            then n < (f . x) by Def13;

            hence thesis by A13, XXREAL_0: 2;

          end;

          then (f . x) = +infty by Th12;

          hence thesis by A11, A12, Def13, XBOOLE_0:def 4;

        end;

        1 in NAT ;

        then 1 in ( dom F) by FUNCT_2:def 1;

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

        then x in (F . 1) by A9, SETFAM_1:def 1;

        then x in (A /\ ( great_dom (f,1))) by A1;

        then

        reconsider x as Element of X;

        x in ( eq_dom (f, +infty )) by A10, Def15;

        hence thesis by A10, XBOOLE_0:def 4;

      end;

      then ( meet ( rng F)) c= (A /\ ( eq_dom (f, +infty )));

      hence thesis by A8, XBOOLE_0:def 10;

    end;

    theorem :: MESFUNC1:24

    

     Th24: for X, S, F, f, A st for n holds (F . n) = (A /\ ( less_dom (f,n))) holds (A /\ ( less_dom (f, +infty ))) = ( union ( rng F))

    proof

      let X, S, F, f, A;

      assume

       A1: for n holds (F . n) = (A /\ ( less_dom (f,n)));

      for x be object st x in (A /\ ( less_dom (f, +infty ))) holds x in ( union ( rng F))

      proof

        let x be object;

        assume

         A2: x in (A /\ ( less_dom (f, +infty )));

        then

         A3: x in A by XBOOLE_0:def 4;

        

         A4: x in ( less_dom (f, +infty )) by A2, XBOOLE_0:def 4;

        then

         A5: x in ( dom f) by Def11;

        

         A6: (f . x) < +infty by A4, Def11;

        ex n be Element of NAT st (f . x) < n

        proof

          per cases ;

            suppose

             A7: (f . x) = -infty ;

            take 0 ;

            thus thesis by A7;

          end;

            suppose not (f . x) = -infty ;

            then not (f . x) <= -infty by XXREAL_0: 6;

            then

            reconsider y1 = (f . x) as Element of REAL by A6, XXREAL_0: 48;

            consider n1 be Element of NAT such that

             A8: y1 <= n1 by Th8;

            

             A9: n1 < (n1 + 1) by NAT_1: 13;

            reconsider m = (n1 + 1) as Element of NAT ;

            take m;

            thus thesis by A8, A9, XXREAL_0: 2;

          end;

        end;

        then

        consider n be Element of NAT such that

         A10: (f . x) < n;

        reconsider x as Element of X by A2;

        x in ( less_dom (f,n)) by A5, A10, Def11;

        then x in (A /\ ( less_dom (f,n))) by A3, XBOOLE_0:def 4;

        then

         A11: x in (F . n) by A1;

        n in NAT ;

        then n in ( dom F) by FUNCT_2:def 1;

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

        hence thesis by A11, TARSKI:def 4;

      end;

      then

       A12: (A /\ ( less_dom (f, +infty ))) c= ( union ( rng F));

      for x be object st x in ( union ( rng F)) holds x in (A /\ ( less_dom (f, +infty )))

      proof

        let x be object;

        assume x in ( union ( rng F));

        then

        consider Y be set such that

         A13: x in Y and

         A14: Y in ( rng F) by TARSKI:def 4;

        consider m such that m in ( dom F) and

         A15: (F . m) = Y by A14, PARTFUN1: 3;

        

         A16: x in (A /\ ( less_dom (f,m))) by A1, A13, A15;

        then

         A17: x in A by XBOOLE_0:def 4;

        

         A18: x in ( less_dom (f,m)) by A16, XBOOLE_0:def 4;

        then

         A19: x in ( dom f) by Def11;

        

         A20: (f . x) < m by A18, Def11;

        reconsider x as Element of X by A13, A14;

        m in REAL by XREAL_0:def 1;

        then (f . x) < +infty by A20, XXREAL_0: 2, XXREAL_0: 9;

        then x in ( less_dom (f, +infty )) by A19, Def11;

        hence thesis by A17, XBOOLE_0:def 4;

      end;

      then ( union ( rng F)) c= (A /\ ( less_dom (f, +infty )));

      hence thesis by A12, XBOOLE_0:def 10;

    end;

    theorem :: MESFUNC1:25

    

     Th25: for X, S, F, f, A st for n be Nat holds (F . n) = (A /\ ( less_dom (f,( - n)))) holds (A /\ ( eq_dom (f, -infty ))) = ( meet ( rng F))

    proof

      let X, S, F, f, A;

      assume

       A1: for n be Nat holds (F . n) = (A /\ ( less_dom (f,( - n))));

      for x be object st x in (A /\ ( eq_dom (f, -infty ))) holds x in ( meet ( rng F))

      proof

        let x be object;

        assume

         A2: x in (A /\ ( eq_dom (f, -infty )));

        then

         A3: x in A by XBOOLE_0:def 4;

        

         A4: x in ( eq_dom (f, -infty )) by A2, XBOOLE_0:def 4;

        for Y be set holds Y in ( rng F) implies x in Y

        proof

          let Y be set;

          Y in ( rng F) implies x in Y

          proof

            assume Y in ( rng F);

            then

            consider m be Element of NAT such that m in ( dom F) and

             A5: Y = (F . m) by PARTFUN1: 3;

            

             A6: Y = (A /\ ( less_dom (f,( - m)))) by A1, A5;

            reconsider x as Element of X by A2;

            

             A7: (f . x) = -infty by A4, Def15;

            ( - m) in REAL by XREAL_0:def 1;

            then x in ( dom f) & not ( - m) <= -infty by A4, Def15, XXREAL_0: 12;

            then x in ( less_dom (f,( - m))) by A7, Def11;

            hence thesis by A3, A6, XBOOLE_0:def 4;

          end;

          hence thesis;

        end;

        hence thesis by SETFAM_1:def 1;

      end;

      then

       A8: (A /\ ( eq_dom (f, -infty ))) c= ( meet ( rng F));

      for x be object st x in ( meet ( rng F)) holds x in (A /\ ( eq_dom (f, -infty )))

      proof

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        assume

         A9: x in ( meet ( rng F));

        

         A10: for m holds x in A & x in ( dom f) & ex y be R_eal st y = (f . x) & y = -infty

        proof

          let m;

          m in NAT ;

          then m in ( dom F) by FUNCT_2:def 1;

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

          then x in (F . m) by A9, SETFAM_1:def 1;

          then

           A11: x in (A /\ ( less_dom (f,( - m)))) by A1;

          then

           A12: x in ( less_dom (f,( - m))) by XBOOLE_0:def 4;

          for r holds (f . xx) < r

          proof

            let r;

            consider n be Nat such that

             A13: ( - n) <= r by Th9;

            n in NAT by ORDINAL1:def 12;

            then n in ( dom F) by FUNCT_2:def 1;

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

            then x in (F . n) by A9, SETFAM_1:def 1;

            then x in (A /\ ( less_dom (f,( - n)))) by A1;

            then x in ( less_dom (f,( - n))) by XBOOLE_0:def 4;

            then (f . x) < ( - n) by Def11;

            hence thesis by A13, XXREAL_0: 2;

          end;

          then (f . x) = -infty by Th13;

          hence thesis by A11, A12, Def11, XBOOLE_0:def 4;

        end;

        1 in NAT ;

        then 1 in ( dom F) by FUNCT_2:def 1;

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

        then x in (F . 1) by A9, SETFAM_1:def 1;

        then x in (A /\ ( less_dom (f,( - 1)))) by A1;

        then

        reconsider x as Element of X;

        x in ( eq_dom (f, -infty )) by A10, Def15;

        hence thesis by A10, XBOOLE_0:def 4;

      end;

      then ( meet ( rng F)) c= (A /\ ( eq_dom (f, -infty )));

      hence thesis by A8, XBOOLE_0:def 10;

    end;

    theorem :: MESFUNC1:26

    

     Th26: for X, S, F, f, A st for n holds (F . n) = (A /\ ( great_dom (f,( - n)))) holds (A /\ ( great_dom (f, -infty ))) = ( union ( rng F))

    proof

      let X, S, F, f, A;

      assume

       A1: for n holds (F . n) = (A /\ ( great_dom (f,( - n))));

      for x be object st x in (A /\ ( great_dom (f, -infty ))) holds x in ( union ( rng F))

      proof

        let x be object;

        assume

         A2: x in (A /\ ( great_dom (f, -infty )));

        then

         A3: x in A by XBOOLE_0:def 4;

        

         A4: x in ( great_dom (f, -infty )) by A2, XBOOLE_0:def 4;

        then

         A5: x in ( dom f) by Def13;

        

         A6: -infty < (f . x) by A4, Def13;

        ex n be Element of NAT st ( - n) < (f . x)

        proof

          per cases ;

            suppose

             A7: (f . x) = +infty ;

            take 0 ;

            thus thesis by A7;

          end;

            suppose not (f . x) = +infty ;

            then not +infty <= (f . x) by XXREAL_0: 4;

            then

            reconsider y1 = (f . x) as Element of REAL by A6, XXREAL_0: 48;

            consider n1 be Nat such that

             A8: ( - n1) <= y1 by Th9;

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

            then

             A9: ( - (n1 + 1)) < ( - n1) by XREAL_1: 24;

            reconsider m = (n1 + 1) as Element of NAT ;

            take m;

            thus thesis by A8, A9, XXREAL_0: 2;

          end;

        end;

        then

        consider n be Element of NAT such that

         A10: ( - n) < (f . x);

        reconsider x as Element of X by A2;

        x in ( great_dom (f,( - n))) by A5, A10, Def13;

        then x in (A /\ ( great_dom (f,( - n)))) by A3, XBOOLE_0:def 4;

        then

         A11: x in (F . n) by A1;

        n in NAT ;

        then n in ( dom F) by FUNCT_2:def 1;

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

        hence thesis by A11, TARSKI:def 4;

      end;

      then

       A12: (A /\ ( great_dom (f, -infty ))) c= ( union ( rng F));

      for x be object st x in ( union ( rng F)) holds x in (A /\ ( great_dom (f, -infty )))

      proof

        let x be object;

        assume x in ( union ( rng F));

        then

        consider Y be set such that

         A13: x in Y and

         A14: Y in ( rng F) by TARSKI:def 4;

        consider m such that m in ( dom F) and

         A15: (F . m) = Y by A14, PARTFUN1: 3;

        

         A16: x in (A /\ ( great_dom (f,( - m)))) by A1, A13, A15;

        then

         A17: x in A by XBOOLE_0:def 4;

        

         A18: x in ( great_dom (f,( - m))) by A16, XBOOLE_0:def 4;

        then

         A19: x in ( dom f) by Def13;

        

         A20: ( - m) < (f . x) by A18, Def13;

        reconsider x as Element of X by A13, A14;

        ( - m) in REAL by XREAL_0:def 1;

        then -infty < (f . x) by A20, XXREAL_0: 2, XXREAL_0: 12;

        then x in ( great_dom (f, -infty )) by A19, Def13;

        hence thesis by A17, XBOOLE_0:def 4;

      end;

      then ( union ( rng F)) c= (A /\ ( great_dom (f, -infty )));

      hence thesis by A12, XBOOLE_0:def 10;

    end;

    begin

    definition

      let X be non empty set;

      let S be SigmaField of X;

      let A be Element of S;

      let f be PartFunc of X, ExtREAL ;

      :: MESFUNC1:def15

      attr f is A -measurable means for r be Real holds (A /\ ( less_dom (f,r))) in S;

    end

    reserve X for non empty set;

    reserve x for Element of X;

    reserve f,g for PartFunc of X, ExtREAL ;

    reserve S for SigmaField of X;

    reserve A,B for Element of S;

    theorem :: MESFUNC1:27

    for X, S, f, A st A c= ( dom f) holds f is A -measurable iff for r be Real holds (A /\ ( great_eq_dom (f,r))) in S

    proof

      let X, S, f, A;

      assume

       A1: A c= ( dom f);

      

       A2: f is A -measurable implies for r be Real holds (A /\ ( great_eq_dom (f,r))) in S

      proof

        assume

         A3: f is A -measurable;

        for r be Real holds (A /\ ( great_eq_dom (f,r))) in S

        proof

          let r be Real;

          (A /\ ( less_dom (f,r))) in S & (A /\ ( great_eq_dom (f,r))) = (A \ (A /\ ( less_dom (f,r)))) by A1, A3, Th14;

          hence thesis by MEASURE1: 6;

        end;

        hence thesis;

      end;

      (for r be Real holds (A /\ ( great_eq_dom (f,r))) in S) implies f is A -measurable

      proof

        assume

         A4: for r be Real holds (A /\ ( great_eq_dom (f,r))) in S;

        for r be Real holds (A /\ ( less_dom (f,r))) in S

        proof

          let r be Real;

          (A /\ ( great_eq_dom (f,r))) in S & (A /\ ( less_dom (f,r))) = (A \ (A /\ ( great_eq_dom (f,r)))) by A1, A4, Th17;

          hence thesis by MEASURE1: 6;

        end;

        hence thesis;

      end;

      hence thesis by A2;

    end;

    theorem :: MESFUNC1:28

    

     Th28: for X, S, f, A holds f is A -measurable iff for r be Real holds (A /\ ( less_eq_dom (f,r))) in S

    proof

      let X, S, f, A;

      

       A1: f is A -measurable implies for r be Real holds (A /\ ( less_eq_dom (f,r))) in S

      proof

        assume

         A2: f is A -measurable;

        for r be Real holds (A /\ ( less_eq_dom (f,r))) in S

        proof

          let r be Real;

          defpred P[ Element of NAT , set] means (A /\ ( less_dom (f,(r + (1 / ($1 + 1)))))) = $2;

          

           A3: for n holds ex y be Element of S st P[n, y]

          proof

            let n;

            reconsider y = (A /\ ( less_dom (f,(r + (1 / (n + 1)))))) as Element of S by A2;

            take y;

            thus thesis;

          end;

          consider F be sequence of S such that

           A4: for n holds P[n, (F . n)] from FUNCT_2:sch 3( A3);

          (A /\ ( less_eq_dom (f,r))) = ( meet ( rng F)) by A4, Th20;

          hence thesis;

        end;

        hence thesis;

      end;

      (for r be Real holds (A /\ ( less_eq_dom (f,r))) in S) implies f is A -measurable

      proof

        assume

         A5: for r be Real holds (A /\ ( less_eq_dom (f,r))) in S;

        for r be Real holds (A /\ ( less_dom (f,r))) in S

        proof

          let r be Real;

          defpred P[ Element of NAT , set] means (A /\ ( less_eq_dom (f,(r - (1 / ($1 + 1)))))) = $2;

          

           A6: for n holds ex y be Element of S st P[n, y]

          proof

            let n;

            reconsider y = (A /\ ( less_eq_dom (f,(r - (1 / (n + 1)))))) as Element of S by A5;

            take y;

            thus thesis;

          end;

          consider F be sequence of S such that

           A7: for n holds P[n, (F . n)] from FUNCT_2:sch 3( A6);

          (A /\ ( less_dom (f,r))) = ( union ( rng F)) by A7, Th21;

          hence thesis;

        end;

        hence thesis;

      end;

      hence thesis by A1;

    end;

    theorem :: MESFUNC1:29

    

     Th29: for X, S, f, A st A c= ( dom f) holds f is A -measurable iff for r be Real holds (A /\ ( great_dom (f,r))) in S

    proof

      let X, S, f, A;

      assume

       A1: A c= ( dom f);

      

       A2: f is A -measurable implies for r be Real holds (A /\ ( great_dom (f,r))) in S

      proof

        assume

         A3: f is A -measurable;

        for r be Real holds (A /\ ( great_dom (f,r))) in S

        proof

          let r be Real;

          (A /\ ( less_eq_dom (f,r))) in S & (A /\ ( great_dom (f,r))) = (A \ (A /\ ( less_eq_dom (f,r)))) by A1, A3, Th15, Th28;

          hence thesis by MEASURE1: 6;

        end;

        hence thesis;

      end;

      (for r be Real holds (A /\ ( great_dom (f,r))) in S) implies f is A -measurable

      proof

        assume

         A4: for r be Real holds (A /\ ( great_dom (f,r))) in S;

        for r be Real holds (A /\ ( less_eq_dom (f,r))) in S

        proof

          let r be Real;

          (A /\ ( great_dom (f,r))) in S & (A /\ ( less_eq_dom (f,r))) = (A \ (A /\ ( great_dom (f,r)))) by A1, A4, Th16;

          hence thesis by MEASURE1: 6;

        end;

        hence thesis by Th28;

      end;

      hence thesis by A2;

    end;

    theorem :: MESFUNC1:30

    for X, S, f, A, B st B c= A & f is A -measurable holds f is B -measurable

    proof

      let X, S, f, A, B;

      assume that

       A1: B c= A and

       A2: f is A -measurable;

      for r be Real holds (B /\ ( less_dom (f,r))) in S

      proof

        let r be Real;

        

         A3: (A /\ ( less_dom (f,r))) in S by A2;

        (B /\ (A /\ ( less_dom (f,r)))) = ((B /\ A) /\ ( less_dom (f,r))) by XBOOLE_1: 16

        .= (B /\ ( less_dom (f,r))) by A1, XBOOLE_1: 28;

        hence thesis by A3, FINSUB_1:def 2;

      end;

      hence thesis;

    end;

    theorem :: MESFUNC1:31

    for X, S, f, A, B st f is A -measurable & f is B -measurable holds f is (A \/ B) -measurable

    proof

      let X, S, f, A, B;

      assume

       A1: f is A -measurable & f is B -measurable;

      for r be Real holds ((A \/ B) /\ ( less_dom (f,r))) in S

      proof

        let r be Real;

        (A /\ ( less_dom (f,r))) in S & (B /\ ( less_dom (f,r))) in S by A1;

        then ((A /\ ( less_dom (f,r))) \/ (B /\ ( less_dom (f,r)))) in S by FINSUB_1:def 1;

        hence thesis by XBOOLE_1: 23;

      end;

      hence thesis;

    end;

    theorem :: MESFUNC1:32

    for X, S, f, A, r, s st f is A -measurable & A c= ( dom f) holds ((A /\ ( great_dom (f,r))) /\ ( less_dom (f,s))) in S

    proof

      let X, S, f, A, r, s;

      assume that

       A1: f is A -measurable and

       A2: A c= ( dom f);

      

       A3: (A /\ ( less_dom (f,s))) in S by A1;

      

       A4: for r1 be Real holds (A /\ ( great_eq_dom (f,r1))) in S

      proof

        let r1 be Real;

        (A /\ ( less_dom (f,r1))) in S & (A /\ ( great_eq_dom (f,r1))) = (A \ (A /\ ( less_dom (f,r1)))) by A1, A2, Th14;

        hence thesis by MEASURE1: 6;

      end;

      for r1 holds (A /\ ( great_dom (f,r1))) in S

      proof

        let r1;

        defpred P[ Element of NAT , set] means (A /\ ( great_eq_dom (f,(r1 + (1 / ($1 + 1)))))) = $2;

        

         A5: for n holds ex y be Element of S st P[n, y]

        proof

          let n;

          reconsider y = (A /\ ( great_eq_dom (f,(r1 + (1 / (n + 1)))))) as Element of S by A4;

          take y;

          thus thesis;

        end;

        consider F be sequence of S such that

         A6: for n holds P[n, (F . n)] from FUNCT_2:sch 3( A5);

        (A /\ ( great_dom (f,r1))) = ( union ( rng F)) by A6, Th22;

        hence thesis;

      end;

      then

       A7: (A /\ ( great_dom (f,r))) in S;

      ((A /\ ( great_dom (f,r))) /\ (A /\ ( less_dom (f,s)))) = (((A /\ ( great_dom (f,r))) /\ A) /\ ( less_dom (f,s))) by XBOOLE_1: 16

      .= ((( great_dom (f,r)) /\ (A /\ A)) /\ ( less_dom (f,s))) by XBOOLE_1: 16;

      hence thesis by A3, A7, FINSUB_1:def 2;

    end;

    theorem :: MESFUNC1:33

    for X, S, f, A st f is A -measurable & A c= ( dom f) holds (A /\ ( eq_dom (f, +infty ))) in S

    proof

      let X, S, f, A;

      assume

       A1: f is A -measurable & A c= ( dom f);

      defpred P[ Element of NAT , set] means (A /\ ( great_dom (f,$1))) = $2;

      

       A2: for n holds ex y be Element of S st P[n, y]

      proof

        let n;

        reconsider y = (A /\ ( great_dom (f,n))) as Element of S by A1, Th29;

        take y;

        thus thesis;

      end;

      consider F be sequence of S such that

       A3: for n holds P[n, (F . n)] from FUNCT_2:sch 3( A2);

      (A /\ ( eq_dom (f, +infty ))) = ( meet ( rng F)) by A3, Th23;

      hence thesis;

    end;

    theorem :: MESFUNC1:34

    for X, S, f, A st f is A -measurable holds (A /\ ( eq_dom (f, -infty ))) in S

    proof

      let X, S, f, A;

      assume

       A1: f is A -measurable;

      defpred P[ Nat, set] means (A /\ ( less_dom (f,( - $1)))) = $2;

      

       A2: for n holds ex y be Element of S st P[n, y]

      proof

        let n;

        reconsider y = (A /\ ( less_dom (f,( - n)))) as Element of S by A1;

        take y;

        thus thesis;

      end;

      consider F be sequence of S such that

       A3: for n holds P[n, (F . n)] from FUNCT_2:sch 3( A2);

      for n be Nat holds P[n, (F . n)]

      proof

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A3;

      end;

      then (A /\ ( eq_dom (f, -infty ))) = ( meet ( rng F)) by Th25;

      hence thesis;

    end;

    theorem :: MESFUNC1:35

    for X, S, f, A st f is A -measurable & A c= ( dom f) holds ((A /\ ( great_dom (f, -infty ))) /\ ( less_dom (f, +infty ))) in S

    proof

      let X, S, f, A;

      assume that

       A1: f is A -measurable and

       A2: A c= ( dom f);

      

       A3: (A /\ ( great_dom (f, -infty ))) in S

      proof

        defpred P[ Element of NAT , set] means (A /\ ( great_dom (f,( - $1)))) = $2;

        

         A4: for n holds ex y be Element of S st P[n, y]

        proof

          let n;

          reconsider y = (A /\ ( great_dom (f,( - n)))) as Element of S by A1, A2, Th29;

          take y;

          thus thesis;

        end;

        consider F be sequence of S such that

         A5: for n holds P[n, (F . n)] from FUNCT_2:sch 3( A4);

        (A /\ ( great_dom (f, -infty ))) = ( union ( rng F)) by A5, Th26;

        hence thesis;

      end;

      

       A6: (A /\ ( less_dom (f, +infty ))) in S

      proof

        defpred P[ Element of NAT , set] means (A /\ ( less_dom (f,$1))) = $2;

        

         A7: for n holds ex y be Element of S st P[n, y]

        proof

          let n;

          reconsider y = (A /\ ( less_dom (f,n))) as Element of S by A1;

          take y;

          thus thesis;

        end;

        consider F be sequence of S such that

         A8: for n holds P[n, (F . n)] from FUNCT_2:sch 3( A7);

        (A /\ ( less_dom (f, +infty ))) = ( union ( rng F)) by A8, Th24;

        hence thesis;

      end;

      ((A /\ ( great_dom (f, -infty ))) /\ (A /\ ( less_dom (f, +infty )))) = (((A /\ ( great_dom (f, -infty ))) /\ A) /\ ( less_dom (f, +infty ))) by XBOOLE_1: 16

      .= ((( great_dom (f, -infty )) /\ (A /\ A)) /\ ( less_dom (f, +infty ))) by XBOOLE_1: 16;

      hence thesis by A3, A6, FINSUB_1:def 2;

    end;

    theorem :: MESFUNC1:36

    for X, S, f, g, A, r st f is A -measurable & g is A -measurable & A c= ( dom g) holds ((A /\ ( less_dom (f,r))) /\ ( great_dom (g,r))) in S

    proof

      let X, S, f, g, A, r;

      assume f is A -measurable & g is A -measurable & A c= ( dom g);

      then

       A1: (A /\ ( less_dom (f,r))) in S & (A /\ ( great_dom (g,r))) in S by Th29;

      ((A /\ ( less_dom (f,r))) /\ (A /\ ( great_dom (g,r)))) = (((A /\ ( less_dom (f,r))) /\ A) /\ ( great_dom (g,r))) by XBOOLE_1: 16

      .= (((A /\ A) /\ ( less_dom (f,r))) /\ ( great_dom (g,r))) by XBOOLE_1: 16

      .= ((A /\ ( less_dom (f,r))) /\ ( great_dom (g,r)));

      hence thesis by A1, FINSUB_1:def 2;

    end;

    theorem :: MESFUNC1:37

    for X, S, f, A, r st f is A -measurable & A c= ( dom f) holds (r (#) f) is A -measurable

    proof

      let X, S, f, A, r;

      assume that

       A1: f is A -measurable and

       A2: A c= ( dom f);

      for r1 be Real holds (A /\ ( less_dom ((r (#) f),r1))) in S

      proof

        let r1 be Real;

        now

          per cases ;

            suppose

             A3: r <> 0 ;

            reconsider r0 = (r1 / r) as Real;

            

             A4: r1 = (r * r0) by A3, XCMPLX_1: 87;

            now

              per cases by A3;

                suppose

                 A5: r > 0 ;

                for x be Element of X st x in ( less_dom (f,r0)) holds x in ( less_dom ((r (#) f),r1))

                proof

                  let x be Element of X;

                  assume

                   A6: x in ( less_dom (f,r0));

                  then x in ( dom f) by Def11;

                  then

                   A7: x in ( dom (r (#) f)) by Def6;

                  

                   A8: (f . x) < r0 by A6, Def11;

                  (f . x) < (r1 / r) by A8;

                  then

                   A9: ((f . x) * r) < ((r1 / r) * r qua ExtReal) by A5, XXREAL_3: 72;

                  

                   A10: ((r1 / r) * r) = ((r1 / r) * r)

                  .= (r1 / (r / r)) by XCMPLX_1: 81

                  .= (r1 / 1) by A3, XCMPLX_1: 60

                  .= r1;

                  ((r (#) f) . x) = (r * (f . x)) by A7, Def6;

                  hence thesis by A7, A9, A10, Def11;

                end;

                then

                 A11: ( less_dom (f,r0)) c= ( less_dom ((r (#) f),r1));

                for x be Element of X st x in ( less_dom ((r (#) f),r1)) holds x in ( less_dom (f,r0))

                proof

                  let x be Element of X;

                  assume

                   A12: x in ( less_dom ((r (#) f),r1));

                  then

                   A13: x in ( dom (r (#) f)) by Def11;

                  ((r (#) f) . x) < r1 by A12, Def11;

                  then ((r (#) f) . x) < (r * r0) by A4;

                  then

                   A14: (((r (#) f) . x) / r) < ((r * r0) / r qua ExtReal) by A5, XXREAL_3: 80;

                  

                   A15: ((r * r0) / r) = ((r * r0) / r)

                  .= (r0 / (r / r)) by XCMPLX_1: 77

                  .= (r0 / 1) by A3, XCMPLX_1: 60

                  .= r0;

                  x in ( dom f) & (f . x) = (((r (#) f) . x) / r) by A3, A13, Def6, Th6;

                  hence thesis by A14, A15, Def11;

                end;

                then ( less_dom ((r (#) f),r1)) c= ( less_dom (f,r0));

                then ( less_dom (f,r0)) = ( less_dom ((r (#) f),r1)) by A11, XBOOLE_0:def 10;

                hence thesis by A1;

              end;

                suppose

                 A16: r < 0 ;

                for x be Element of X st x in ( great_dom (f,r0)) holds x in ( less_dom ((r (#) f),r1))

                proof

                  let x be Element of X;

                  assume

                   A17: x in ( great_dom (f,r0));

                  then x in ( dom f) by Def13;

                  then

                   A18: x in ( dom (r (#) f)) by Def6;

                  r0 < (f . x) by A17, Def13;

                  then (r1 / r) < (f . x);

                  then

                   A19: ((f . x) * r) < ((r1 / r) * r qua ExtReal) by A16, XXREAL_3: 102;

                  

                   A20: ((r1 / r) * r) = ((r1 / r) * r)

                  .= (r1 / (r / r)) by XCMPLX_1: 81

                  .= (r1 / 1) by A3, XCMPLX_1: 60

                  .= r1;

                  ((r (#) f) . x) = (r * (f . x)) by A18, Def6;

                  hence thesis by A18, A19, A20, Def11;

                end;

                then

                 A21: ( great_dom (f,r0)) c= ( less_dom ((r (#) f),r1));

                for x be Element of X st x in ( less_dom ((r (#) f),r1)) holds x in ( great_dom (f,r0))

                proof

                  let x be Element of X;

                  assume

                   A22: x in ( less_dom ((r (#) f),r1));

                  then

                   A23: x in ( dom (r (#) f)) by Def11;

                  ((r (#) f) . x) < r1 by A22, Def11;

                  then ((r (#) f) . x) < (r * r0) by A4;

                  then

                   A24: ((r * r0) / r qua ExtReal) < (((r (#) f) . x) / r) by A16, XXREAL_3: 104;

                  

                   A25: ((r * r0) / r) = ((r * r0) / r)

                  .= (r0 / (r / r)) by XCMPLX_1: 77

                  .= (r0 / 1) by A3, XCMPLX_1: 60

                  .= r0;

                  x in ( dom f) & (f . x) = (((r (#) f) . x) / r) by A3, A23, Def6, Th6;

                  hence thesis by A24, A25, Def13;

                end;

                then ( less_dom ((r (#) f),r1)) c= ( great_dom (f,r0));

                then ( great_dom (f,r0)) = ( less_dom ((r (#) f),r1)) by A21, XBOOLE_0:def 10;

                hence thesis by A1, A2, Th29;

              end;

            end;

            hence thesis;

          end;

            suppose

             A26: r = 0 ;

            now

              per cases ;

                suppose

                 A27: r1 > 0 ;

                for x1 be object holds x1 in A implies x1 in (A /\ ( less_dom ((r (#) f),r1)))

                proof

                  let x1 be object;

                  assume

                   A28: x1 in A;

                  then

                  reconsider x1 as Element of X;

                  x1 in ( dom f) by A2, A28;

                  then

                   A29: x1 in ( dom (r (#) f)) by Def6;

                  reconsider y = ((r (#) f) . x1) as R_eal;

                  y = (r * (f . x1)) by A29, Def6

                  .= 0. by A26;

                  then x1 in ( less_dom ((r (#) f),r1)) by A27, A29, Def11;

                  hence thesis by A28, XBOOLE_0:def 4;

                end;

                then (A /\ ( less_dom ((r (#) f),r1))) c= A & A c= (A /\ ( less_dom ((r (#) f),r1))) by XBOOLE_1: 17;

                then (A /\ ( less_dom ((r (#) f),r1))) = A by XBOOLE_0:def 10;

                hence thesis;

              end;

                suppose

                 A30: r1 <= 0 ;

                ( less_dom ((r (#) f),r1)) = {}

                proof

                  assume ( less_dom ((r (#) f),r1)) <> {} ;

                  then

                  consider x1 be Element of X such that

                   A31: x1 in ( less_dom ((r (#) f),r1)) by SUBSET_1: 4;

                  

                   A32: x1 in ( dom (r (#) f)) by A31, Def11;

                  

                   A33: ((r (#) f) . x1) < r1 by A31, Def11;

                  

                   A34: ((r (#) f) . x1) in ( rng (r (#) f)) by A32, FUNCT_1:def 3;

                  for y be R_eal st y in ( rng (r (#) f)) holds not y < r1

                  proof

                    let y be R_eal;

                    assume y in ( rng (r (#) f));

                    then

                    consider x such that

                     A35: x in ( dom (r (#) f)) & y = ((r (#) f) . x) by PARTFUN1: 3;

                    y = (r * (f . x)) by A35, Def6

                    .= 0. by A26;

                    hence thesis by A30;

                  end;

                  hence contradiction by A33, A34;

                end;

                hence thesis by PROB_1: 4;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      hence thesis;

    end;