mesfun11.miz



    begin

    registration

      let X be non empty set, f be nonnegative PartFunc of X, ExtREAL ;

      cluster ( - f) -> nonpositive;

      correctness

      proof

        ( - f) = (( - 1) (#) f) by MESFUNC2: 9;

        hence ( - f) is nonpositive by MESFUNC5: 20;

      end;

    end

    registration

      let X be non empty set, f be nonpositive PartFunc of X, ExtREAL ;

      cluster ( - f) -> nonnegative;

      correctness

      proof

        for x be object st x in ( dom ( - f)) holds 0 <= (( - f) . x)

        proof

          let x be object;

          assume

           A1: x in ( dom ( - f));

          (f . x) <= 0 by MESFUNC5: 8;

          then ( - (f . x)) >= 0 ;

          hence (( - f) . x) >= 0 by A1, MESFUNC1:def 7;

        end;

        hence ( - f) is nonnegative by SUPINF_2: 52;

      end;

    end

    theorem :: MESFUN11:1

    

     Th1: for X be non empty set, f be nonpositive PartFunc of X, ExtREAL , E be set holds (f | E) is nonpositive

    proof

      let X be non empty set, f be nonpositive PartFunc of X, ExtREAL , E be set;

      now

        let x be set;

        assume x in ( dom (f | E));

        then ((f | E) . x) = (f . x) by FUNCT_1: 47;

        hence ((f | E) . x) <= 0 by MESFUNC5: 8;

      end;

      hence (f | E) is nonpositive by MESFUNC5: 9;

    end;

    theorem :: MESFUN11:2

    

     Th2: for X be non empty set, A be set, r be Real, f be PartFunc of X, ExtREAL holds ((r (#) f) | A) = (r (#) (f | A))

    proof

      let X be non empty set, A be set, r be Real, f be PartFunc of X, ExtREAL ;

      

       A1: ( dom (r (#) f)) = ( dom f) by MESFUNC1:def 6;

      then

       A2: ( dom ((r (#) f) | A)) = (( dom f) /\ A) by RELAT_1: 61;

      then

       A3: ( dom ((r (#) f) | A)) = ( dom (f | A)) by RELAT_1: 61;

      then

       A4: ( dom ((r (#) f) | A)) = ( dom (r (#) (f | A))) by MESFUNC1:def 6;

      now

        let x be Element of X;

        assume

         B1: x in ( dom ((r (#) f) | A));

        then

         B2: x in ( dom f) by A2, XBOOLE_0:def 4;

        (((r (#) f) | A) . x) = ((r (#) f) . x) by B1, FUNCT_1: 47;

        then (((r (#) f) | A) . x) = (r * (f . x)) by B2, A1, MESFUNC1:def 6;

        then (((r (#) f) | A) . x) = (r * ((f | A) . x)) by B1, A3, FUNCT_1: 47;

        hence (((r (#) f) | A) . x) = ((r (#) (f | A)) . x) by B1, A4, MESFUNC1:def 6;

      end;

      hence ((r (#) f) | A) = (r (#) (f | A)) by A4, PARTFUN1: 5;

    end;

    theorem :: MESFUN11:3

    

     Th3: for X be non empty set, A be set, f be PartFunc of X, ExtREAL holds ( - (f | A)) = (( - f) | A)

    proof

      let X be non empty set, A be set, f be PartFunc of X, ExtREAL ;

      ( - (f | A)) = (( - 1) (#) (f | A)) by MESFUNC2: 9;

      then ( - (f | A)) = ((( - 1) (#) f) | A) by Th2;

      hence thesis by MESFUNC2: 9;

    end;

    theorem :: MESFUN11:4

    

     Th4: for X be non empty set, f be PartFunc of X, ExtREAL , c be Real st f is nonpositive holds ( 0 <= c implies (c (#) f) is nonpositive) & (c <= 0 implies (c (#) f) is nonnegative)

    proof

      let X be non empty set;

      let f be PartFunc of X, ExtREAL ;

      let c be Real;

      set g = (c (#) f);

      assume

       A1: f is nonpositive;

      hereby

        set g = (c (#) f);

        assume

         A2: 0 <= c;

        for x be set st x in ( dom g) holds (g . x) <= 0

        proof

          let x be set;

          (f . x) <= 0 by A1, MESFUNC5: 8;

          then

           A3: (c * (f . x)) <= 0 by A2;

          assume x in ( dom g);

          hence thesis by A3, MESFUNC1:def 6;

        end;

        hence (c (#) f) is nonpositive by MESFUNC5: 9;

      end;

      assume

       A4: c <= 0 ;

      now

        let x be object;

        (f . x) <= 0 by A1, MESFUNC5: 8;

        then

         A5: 0 <= (c * (f . x)) by A4;

        assume x in ( dom g);

        hence 0 <= (g . x) by A5, MESFUNC1:def 6;

      end;

      hence thesis by SUPINF_2: 52;

    end;

    theorem :: MESFUN11:5

    

     Th5: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, ExtREAL holds ( max+ f) is nonnegative & ( max- f) is nonnegative & |.f.| is nonnegative

    proof

      let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, ExtREAL ;

      

       A1: for x be object st x in ( dom ( max- f)) holds 0 <= (( max- f) . x) by MESFUNC2: 13;

      for x be object st x in ( dom ( max+ f)) holds 0 <= (( max+ f) . x) by MESFUNC2: 12;

      hence ( max+ f) is nonnegative & ( max- f) is nonnegative by A1, SUPINF_2: 52;

      now

        let x be object;

        assume x in ( dom |.f.|);

        then ( |.f.| . x) = |.(f . x).| by MESFUNC1:def 10;

        hence 0 <= ( |.f.| . x) by EXTREAL1: 14;

      end;

      hence thesis by SUPINF_2: 52;

    end;

    theorem :: MESFUN11:6

    for X be non empty set, f be PartFunc of X, ExtREAL , x be object holds (f . x) <= (( max+ f) . x) & (f . x) >= ( - (( max- f) . x))

    proof

      let X be non empty set, f be PartFunc of X, ExtREAL , x be object;

      per cases ;

        suppose x in ( dom f);

        then x in ( dom ( max+ f)) & x in ( dom ( max- f)) by MESFUNC2:def 2, MESFUNC2:def 3;

        then

         A1: (( max+ f) . x) = ( max ((f . x), 0 )) & (( max- f) . x) = ( max (( - (f . x)), 0 )) by MESFUNC2:def 2, MESFUNC2:def 3;

        reconsider a = (( max- f) . x), b = ( - (f . x)) as ExtReal;

        ( - b) >= ( - a) by A1, XXREAL_0: 25, XXREAL_3: 38;

        hence (f . x) <= (( max+ f) . x) & (f . x) >= ( - (( max- f) . x)) by A1, XXREAL_0: 25;

      end;

        suppose

         A2: not x in ( dom f);

        then not x in ( dom ( max+ f)) & not x in ( dom ( max- f)) by MESFUNC2:def 2, MESFUNC2:def 3;

        then (f . x) = 0 & (( max+ f) . x) = 0 & (( max- f) . x) = 0 by A2, FUNCT_1:def 2;

        hence (f . x) <= (( max+ f) . x) & (f . x) >= ( - (( max- f) . x));

      end;

    end;

    

     Lm1: for X be non empty set, f be PartFunc of X, ExtREAL , r be Real holds (r > 0 implies ( less_dom (f,r)) = ( less_dom (( max+ f),r))) & (r <= 0 implies ( less_dom (f,r)) = ( great_dom (( max- f),( - r))))

    proof

      let X be non empty set, f be PartFunc of X, ExtREAL , r be Real;

      hereby

        assume

         A1: r > 0 ;

        reconsider r1 = r as ExtReal;

        now

          let x be Element of X;

          assume x in ( less_dom (( max+ f),r));

          then

           A2: x in ( dom ( max+ f)) & (( max+ f) . x) < r by MESFUNC1:def 11;

          then

           A3: x in ( dom f) by MESFUNC2:def 2;

          ( max ((f . x), 0 )) < r1 by A2, MESFUNC2:def 2;

          then (f . x) < r1 by XXREAL_0: 31;

          hence x in ( less_dom (f,r)) by A3, MESFUNC1:def 11;

        end;

        then

         A4: ( less_dom (( max+ f),r)) c= ( less_dom (f,r));

        now

          let x be Element of X;

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

          then

           A5: x in ( dom f) & (f . x) < r by MESFUNC1:def 11;

          then

           A6: x in ( dom ( max+ f)) by MESFUNC2:def 2;

          then (( max+ f) . x) = ( max ((f . x), 0 )) by MESFUNC2:def 2;

          then (( max+ f) . x) < r by A1, A5, XXREAL_0: 29;

          hence x in ( less_dom (( max+ f),r)) by A6, MESFUNC1:def 11;

        end;

        then ( less_dom (f,r)) c= ( less_dom (( max+ f),r));

        hence ( less_dom (( max+ f),r)) = ( less_dom (f,r)) by A4;

      end;

      assume

       A7: r <= 0 ;

      reconsider r1 = r as ExtReal;

      now

        let x be Element of X;

        assume x in ( great_dom (( max- f),( - r)));

        then

         A8: x in ( dom ( max- f)) & (( max- f) . x) > ( - r) by MESFUNC1:def 13;

        then

         A9: x in ( dom f) by MESFUNC2:def 3;

        

         A10: ( max (( - (f . x)), 0 )) > ( - r1) by A8, MESFUNC2:def 3;

        now

          assume 0 > ( - (f . x));

          then ( max (( - (f . x)), 0 )) = 0 by XXREAL_0:def 10;

          hence contradiction by A7, A10;

        end;

        then ( max (( - (f . x)), 0 )) = ( - (f . x)) by XXREAL_0:def 10;

        then (f . x) < r1 by A10, XXREAL_3: 38;

        hence x in ( less_dom (f,r)) by A9, MESFUNC1:def 11;

      end;

      then

       A11: ( great_dom (( max- f),( - r))) c= ( less_dom (f,r));

      now

        let x be Element of X;

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

        then

         A12: x in ( dom f) & (f . x) < r by MESFUNC1:def 11;

        then

         A13: x in ( dom ( max- f)) by MESFUNC2:def 3;

        ( max (( - (f . x)), 0 )) = ( - (f . x)) by A7, A12, XXREAL_0:def 10;

        then (( max- f) . x) = ( - (f . x)) by A13, MESFUNC2:def 3;

        then (( max- f) . x) > ( - r1) by A12, XXREAL_3: 38;

        hence x in ( great_dom (( max- f),( - r))) by A13, MESFUNC1:def 13;

      end;

      then ( less_dom (f,r)) c= ( great_dom (( max- f),( - r)));

      hence ( great_dom (( max- f),( - r))) = ( less_dom (f,r)) by A11;

    end;

    theorem :: MESFUN11:7

    for X be non empty set, f be PartFunc of X, ExtREAL , r be positive Real holds ( less_dom (f,r)) = ( less_dom (( max+ f),r)) by Lm1;

    theorem :: MESFUN11:8

    for X be non empty set, f be PartFunc of X, ExtREAL , r be non positive Real holds ( less_dom (f,r)) = ( great_dom (( max- f),( - r))) by Lm1;

    theorem :: MESFUN11:9

    

     Th9: for X be non empty set, f,g be PartFunc of X, ExtREAL , a be ExtReal, r be Real st r <> 0 & g = (r (#) f) holds ( eq_dom (f,a)) = ( eq_dom (g,(a * r)))

    proof

      let X be non empty set, f,g be PartFunc of X, ExtREAL , a be ExtReal, r be Real;

      assume that

       A1: r <> 0 and

       a2: g = (r (#) f);

      

       A2: ( dom f) = ( dom g) by a2, MESFUNC1:def 6;

      now

        let x be object;

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

        then x in ( dom f) & (f . x) = a by MESFUNC1:def 15;

        then x in ( dom g) & (g . x) = (r * a) by a2, A2, MESFUNC1:def 6;

        hence x in ( eq_dom (g,(a * r))) by MESFUNC1:def 15;

      end;

      then

       A3: ( eq_dom (f,a)) c= ( eq_dom (g,(a * r)));

      now

        let x be object;

        assume x in ( eq_dom (g,(a * r)));

        then

         A4: x in ( dom g) & (g . x) = (a * r) by MESFUNC1:def 15;

        then (r * (f . x)) = (a * r) by a2, MESFUNC1:def 6;

        then (f . x) = a by A1, XXREAL_3: 68;

        hence x in ( eq_dom (f,a)) by A2, A4, MESFUNC1:def 15;

      end;

      then ( eq_dom (g,(a * r))) c= ( eq_dom (f,a));

      hence thesis by A3;

    end;

    theorem :: MESFUN11:10

    

     Th10: for X be non empty set, S be SigmaField of X, f be PartFunc of X, ExtREAL , A be Element of S st A c= ( dom f) holds f is A -measurable iff ( max+ f) is A -measurable & ( max- f) is A -measurable

    proof

      let X be non empty set, S be SigmaField of X, f be PartFunc of X, ExtREAL , A be Element of S;

      assume

       A1: A c= ( dom f);

      hence f is A -measurable implies ( max+ f) is A -measurable & ( max- f) is A -measurable by MESFUNC2: 25, MESFUNC2: 26;

      assume

       A2: ( max+ f) is A -measurable & ( max- f) is A -measurable;

      

       A3: ( dom ( max- f)) = ( dom f) by MESFUNC2:def 3;

      now

        let r be Real;

        per cases ;

          suppose r > 0 ;

          then ( less_dom (f,r)) = ( less_dom (( max+ f),r)) by Lm1;

          hence (A /\ ( less_dom (f,r))) in S by A2, MESFUNC1:def 16;

        end;

          suppose r <= 0 ;

          then ( less_dom (f,r)) = ( great_dom (( max- f),( - r))) by Lm1;

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

        end;

      end;

      hence f is A -measurable by MESFUNC1:def 16;

    end;

    

     Lm2: for i,j be Nat st i <= j holds ex k be Nat st j = (i + k)

    proof

      let i,j be Nat;

      defpred P[ Nat] means i <= $1 implies ex k be Nat st $1 = (i + k);

      

       A1: for j be Nat st P[j] holds P[(j + 1)]

      proof

        let j be Nat such that

         A2: i <= j implies ex k be Nat st j = (i + k);

        assume

         A3: i <= (j + 1);

        per cases by A3, NAT_1: 8;

          suppose i <= j;

          then

          consider k be Nat such that

           A4: j = (i + k) by A2;

          reconsider k1 = (k + 1) as Nat;

          take k1;

          thus (j + 1) = (i + k1) by A4;

        end;

          suppose

           B1: i = (j + 1);

          reconsider k1 = 0 as Nat;

          take k1;

          thus (j + 1) = (i + k1) by B1;

        end;

      end;

      

       A6: P[ 0 ]

      proof

        assume

         A7: i <= 0 ;

        take 0 ;

        thus thesis by A7;

      end;

      for j be Nat holds P[j] from NAT_1:sch 2( A6, A1);

      hence thesis;

    end;

    definition

      let X be non empty set, f be Function of X, ExtREAL , r be Real;

      :: original: (#)

      redefine

      func r (#) f -> Function of X, ExtREAL ;

      correctness

      proof

        ( dom (r (#) f)) = ( dom f) by MESFUNC1:def 6;

        then ( dom (r (#) f)) = X by FUNCT_2:def 1;

        hence (r (#) f) is Function of X, ExtREAL by FUNCT_2:def 1;

      end;

    end

    theorem :: MESFUN11:11

    

     Th11: for X be non empty set, r be Real, f be without+infty Function of X, ExtREAL st r >= 0 holds (r (#) f) is without+infty

    proof

      let X be non empty set, r be Real, f be without+infty Function of X, ExtREAL ;

      assume

       A1: r >= 0 ;

      now

        let x be set;

        assume

         A2: x in ( dom (r (#) f));

        then

         A3: x in ( dom f) by MESFUNC1:def 6;

        per cases by A1;

          suppose

           A4: r > 0 ;

          then (r * (f . x)) < (r * +infty ) by A3, MESFUNC5: 11, XXREAL_3: 72;

          then (r * (f . x)) < +infty by A4, XXREAL_3:def 5;

          hence ((r (#) f) . x) < +infty by A2, MESFUNC1:def 6;

        end;

          suppose r = 0 ;

          then (r * (f . x)) < +infty ;

          hence ((r (#) f) . x) < +infty by A2, MESFUNC1:def 6;

        end;

      end;

      hence (r (#) f) is without+infty by MESFUNC5: 11;

    end;

    registration

      let X be non empty set;

      let f be without+infty Function of X, ExtREAL ;

      let r be non negative Real;

      cluster (r (#) f) -> without+infty;

      coherence by Th11;

    end

    theorem :: MESFUN11:12

    

     Th12: for X be non empty set, r be Real, f be without+infty Function of X, ExtREAL st r <= 0 holds (r (#) f) is without-infty

    proof

      let X be non empty set, r be Real, f be without+infty Function of X, ExtREAL ;

      assume

       A1: r <= 0 ;

      now

        let x be set;

        assume

         A2: x in ( dom (r (#) f));

        then

         A3: x in ( dom f) by MESFUNC1:def 6;

        per cases by A1;

          suppose

           A4: r < 0 ;

          then (r * (f . x)) > (r * +infty ) by A3, MESFUNC5: 11, XXREAL_3: 102;

          then (r * (f . x)) > -infty by A4, XXREAL_3:def 5;

          hence ((r (#) f) . x) > -infty by A2, MESFUNC1:def 6;

        end;

          suppose r = 0 ;

          then (r * (f . x)) > -infty ;

          hence ((r (#) f) . x) > -infty by A2, MESFUNC1:def 6;

        end;

      end;

      hence (r (#) f) is without-infty by MESFUNC5: 10;

    end;

    registration

      let X be non empty set;

      let f be without+infty Function of X, ExtREAL ;

      let r be non positive Real;

      cluster (r (#) f) -> without-infty;

      correctness by Th12;

    end

    theorem :: MESFUN11:13

    

     Th13: for X be non empty set, r be Real, f be without-infty Function of X, ExtREAL st r >= 0 holds (r (#) f) is without-infty

    proof

      let X be non empty set, r be Real, f be without-infty Function of X, ExtREAL ;

      assume

       A1: r >= 0 ;

      now

        let x be set;

        assume

         A2: x in ( dom (r (#) f));

        then

         A3: x in ( dom f) by MESFUNC1:def 6;

        per cases by A1;

          suppose

           A4: r > 0 ;

          then (r * (f . x)) > (r * -infty ) by A3, MESFUNC5: 10, XXREAL_3: 72;

          then (r * (f . x)) > -infty by A4, XXREAL_3:def 5;

          hence ((r (#) f) . x) > -infty by A2, MESFUNC1:def 6;

        end;

          suppose r = 0 ;

          then (r * (f . x)) > -infty ;

          hence ((r (#) f) . x) > -infty by A2, MESFUNC1:def 6;

        end;

      end;

      hence (r (#) f) is without-infty by MESFUNC5: 10;

    end;

    registration

      let X be non empty set;

      let f be without-infty Function of X, ExtREAL ;

      let r be non negative Real;

      cluster (r (#) f) -> without-infty;

      correctness by Th13;

    end

    theorem :: MESFUN11:14

    

     Th14: for X be non empty set, r be Real, f be without-infty Function of X, ExtREAL st r <= 0 holds (r (#) f) is without+infty

    proof

      let X be non empty set, r be Real, f be without-infty Function of X, ExtREAL ;

      assume

       A1: r <= 0 ;

      now

        let x be set;

        assume

         A2: x in ( dom (r (#) f));

        then

         A3: x in ( dom f) by MESFUNC1:def 6;

        per cases by A1;

          suppose

           A4: r < 0 ;

          then (r * (f . x)) < (r * -infty ) by A3, MESFUNC5: 10, XXREAL_3: 102;

          then (r * (f . x)) < +infty by A4, XXREAL_3:def 5;

          hence ((r (#) f) . x) < +infty by A2, MESFUNC1:def 6;

        end;

          suppose r = 0 ;

          then (r * (f . x)) < +infty ;

          hence ((r (#) f) . x) < +infty by A2, MESFUNC1:def 6;

        end;

      end;

      hence (r (#) f) is without+infty by MESFUNC5: 11;

    end;

    registration

      let X be non empty set;

      let f be without-infty Function of X, ExtREAL ;

      let r be non positive Real;

      cluster (r (#) f) -> without+infty;

      correctness by Th14;

    end

    theorem :: MESFUN11:15

    

     Th15: for X be non empty set, r be Real, f be without-infty without+infty Function of X, ExtREAL holds (r (#) f) is without-infty without+infty

    proof

      let X be non empty set, r be Real, f be without-infty without+infty Function of X, ExtREAL ;

      per cases ;

        suppose r >= 0 ;

        hence (r (#) f) is without-infty without+infty;

      end;

        suppose r < 0 ;

        hence (r (#) f) is without-infty without+infty;

      end;

    end;

    registration

      let X be non empty set;

      let f be without-infty without+infty Function of X, ExtREAL ;

      let r be Real;

      cluster (r (#) f) -> without-infty without+infty;

      correctness by Th15;

    end

    theorem :: MESFUN11:16

    

     Th16: for X be non empty set, r be positive Real, f be Function of X, ExtREAL holds f is without+infty iff (r (#) f) is without+infty

    proof

      let X be non empty set, r be positive Real, f be Function of X, ExtREAL ;

      thus f is without+infty implies (r (#) f) is without+infty;

      assume

       A2: (r (#) f) is without+infty;

      now

        let x be set;

        assume x in ( dom f);

        then

         A3: x in ( dom (r (#) f)) by MESFUNC1:def 6;

        then ((r (#) f) . x) = (r * (f . x)) by MESFUNC1:def 6;

        then (r * (f . x)) < +infty by A2, A3, MESFUNC5: 11;

        then (f . x) <> +infty by XXREAL_3:def 5;

        hence (f . x) < +infty by XXREAL_0: 4;

      end;

      hence f is without+infty by MESFUNC5: 11;

    end;

    theorem :: MESFUN11:17

    

     Th17: for X be non empty set, r be negative Real, f be Function of X, ExtREAL holds f is without+infty iff (r (#) f) is without-infty

    proof

      let X be non empty set, r be negative Real, f be Function of X, ExtREAL ;

      thus f is without+infty implies (r (#) f) is without-infty;

      assume

       A2: (r (#) f) is without-infty;

      now

        let x be set;

        assume x in ( dom f);

        then

         A3: x in ( dom (r (#) f)) by MESFUNC1:def 6;

        then ((r (#) f) . x) = (r * (f . x)) by MESFUNC1:def 6;

        then (r * (f . x)) > -infty by A2, A3, MESFUNC5: 10;

        then (f . x) <> +infty by XXREAL_3:def 5;

        hence (f . x) < +infty by XXREAL_0: 4;

      end;

      hence f is without+infty by MESFUNC5: 11;

    end;

    theorem :: MESFUN11:18

    

     Th18: for X be non empty set, r be positive Real, f be Function of X, ExtREAL holds f is without-infty iff (r (#) f) is without-infty

    proof

      let X be non empty set, r be positive Real, f be Function of X, ExtREAL ;

      thus f is without-infty implies (r (#) f) is without-infty;

      assume

       A2: (r (#) f) is without-infty;

      now

        let x be set;

        assume x in ( dom f);

        then

         A3: x in ( dom (r (#) f)) by MESFUNC1:def 6;

        then ((r (#) f) . x) = (r * (f . x)) by MESFUNC1:def 6;

        then (r * (f . x)) > -infty by A2, A3, MESFUNC5: 10;

        then (f . x) <> -infty by XXREAL_3:def 5;

        hence (f . x) > -infty by XXREAL_0: 6;

      end;

      hence f is without-infty by MESFUNC5: 10;

    end;

    theorem :: MESFUN11:19

    

     Th19: for X be non empty set, r be negative Real, f be Function of X, ExtREAL holds f is without-infty iff (r (#) f) is without+infty

    proof

      let X be non empty set, r be negative Real, f be Function of X, ExtREAL ;

      thus f is without-infty implies (r (#) f) is without+infty;

      assume

       A2: (r (#) f) is without+infty;

      now

        let x be set;

        assume x in ( dom f);

        then

         A3: x in ( dom (r (#) f)) by MESFUNC1:def 6;

        then ((r (#) f) . x) = (r * (f . x)) by MESFUNC1:def 6;

        then (r * (f . x)) < +infty by A2, A3, MESFUNC5: 11;

        then (f . x) <> -infty by XXREAL_3:def 5;

        hence (f . x) > -infty by XXREAL_0: 6;

      end;

      hence f is without-infty by MESFUNC5: 10;

    end;

    theorem :: MESFUN11:20

    for X be non empty set, r be non zero Real, f be Function of X, ExtREAL holds f is without-infty without+infty iff (r (#) f) is without-infty without+infty

    proof

      let X be non empty set, r be non zero Real, f be Function of X, ExtREAL ;

      per cases ;

        suppose r > 0 ;

        hence f is without-infty without+infty iff (r (#) f) is without-infty without+infty by Th16, Th18;

      end;

        suppose r < 0 ;

        hence f is without-infty without+infty iff (r (#) f) is without-infty without+infty by Th17, Th19;

      end;

    end;

    theorem :: MESFUN11:21

    

     Th21: for X,Y be non empty set, f be PartFunc of X, ExtREAL , r be Real st f = (Y --> r) holds f is without-infty without+infty

    proof

      let X,Y be non empty set, f be PartFunc of X, ExtREAL , r be Real;

      assume

       A1: f = (Y --> r);

      then for x be object holds (f . x) > -infty by XREAL_0:def 1, XXREAL_0: 12;

      hence f is without-infty by MESFUNC5:def 5;

      for x be object holds (f . x) < +infty by A1, XREAL_0:def 1, XXREAL_0: 9;

      hence f is without+infty by MESFUNC5:def 6;

    end;

    theorem :: MESFUN11:22

    for X be non empty set, f be Function of X, ExtREAL holds ( 0 (#) f) = (X --> 0 ) & ( 0 (#) f) is without-infty without+infty

    proof

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

      

       A1: (X --> 0 ) is Function of X, ExtREAL by FUNCOP_1: 45, XXREAL_0:def 1;

      for x be Element of X holds (( 0 (#) f) . x) = ((X --> 0 ) . x)

      proof

        let x be Element of X;

        x in X;

        then x in ( dom ( 0 (#) f)) by FUNCT_2:def 1;

        then (( 0 (#) f) . x) = ( 0 * (f . x)) by MESFUNC1:def 6;

        hence (( 0 (#) f) . x) = ((X --> 0 ) . x) by FUNCOP_1: 7;

      end;

      hence ( 0 (#) f) = (X --> 0 ) by A1, FUNCT_2:def 8;

      hence ( 0 (#) f) is without-infty without+infty by Th21;

    end;

    theorem :: MESFUN11:23

    

     Th23: for X be non empty set, f,g be PartFunc of X, ExtREAL st f is without-infty without+infty holds ( dom (f + g)) = (( dom f) /\ ( dom g)) & ( dom (f - g)) = (( dom f) /\ ( dom g)) & ( dom (g - f)) = (( dom f) /\ ( dom g))

    proof

      let X be non empty set, f,g be PartFunc of X, ExtREAL ;

      assume

       A1: f is without-infty without+infty;

      then not -infty in ( rng f) by MESFUNC5:def 3;

      then

       A2: (f " { -infty }) = {} by FUNCT_1: 72;

       not +infty in ( rng f) by A1, MESFUNC5:def 4;

      then

       A3: (f " { +infty }) = {} by FUNCT_1: 72;

      then (((f " { +infty }) /\ (g " { -infty })) \/ ((f " { -infty }) /\ (g " { +infty }))) = {} by A2;

      then ( dom (f + g)) = ((( dom f) /\ ( dom g)) \ {} ) by MESFUNC1:def 3;

      hence ( dom (f + g)) = (( dom f) /\ ( dom g));

      

       A4: (((f " { +infty }) /\ (g " { +infty })) \/ ((f " { -infty }) /\ (g " { -infty }))) = {} by A2, A3;

      then ( dom (f - g)) = ((( dom f) /\ ( dom g)) \ {} ) by MESFUNC1:def 4;

      hence ( dom (f - g)) = (( dom f) /\ ( dom g));

      ( dom (g - f)) = ((( dom f) /\ ( dom g)) \ {} ) by A4, MESFUNC1:def 4;

      hence ( dom (g - f)) = (( dom f) /\ ( dom g));

    end;

    theorem :: MESFUN11:24

    for X be non empty set, f1,f2 be Function of X, ExtREAL st f2 is without-infty without+infty holds (f1 + f2) is Function of X, ExtREAL & for x be Element of X holds ((f1 + f2) . x) = ((f1 . x) + (f2 . x))

    proof

      let X be non empty set, f1,f2 be Function of X, ExtREAL ;

      assume

       A1: f2 is without-infty without+infty;

      ( dom f1) = X & ( dom f2) = X by FUNCT_2:def 1;

      then

       A2: ( dom (f1 + f2)) = (X /\ X) by A1, Th23;

      hence (f1 + f2) is Function of X, ExtREAL by FUNCT_2:def 1;

      thus thesis by A2, MESFUNC1:def 3;

    end;

    theorem :: MESFUN11:25

    for X be non empty set, f1,f2 be Function of X, ExtREAL st f1 is without-infty without+infty holds (f1 - f2) is Function of X, ExtREAL & for x be Element of X holds ((f1 - f2) . x) = ((f1 . x) - (f2 . x))

    proof

      let X be non empty set, f1,f2 be Function of X, ExtREAL ;

      assume

       A1: f1 is without-infty without+infty;

      ( dom f1) = X & ( dom f2) = X by FUNCT_2:def 1;

      then

       A2: ( dom (f1 - f2)) = (X /\ X) by A1, Th23;

      hence (f1 - f2) is Function of X, ExtREAL by FUNCT_2:def 1;

      thus thesis by A2, MESFUNC1:def 4;

    end;

    theorem :: MESFUN11:26

    for X be non empty set, f1,f2 be Function of X, ExtREAL st f2 is without-infty without+infty holds (f1 - f2) is Function of X, ExtREAL & for x be Element of X holds ((f1 - f2) . x) = ((f1 . x) - (f2 . x))

    proof

      let X be non empty set, f1,f2 be Function of X, ExtREAL ;

      assume

       A1: f2 is without-infty without+infty;

      ( dom f1) = X & ( dom f2) = X by FUNCT_2:def 1;

      then

       A2: ( dom (f1 - f2)) = (X /\ X) by A1, Th23;

      hence (f1 - f2) is Function of X, ExtREAL by FUNCT_2:def 1;

      thus thesis by A2, MESFUNC1:def 4;

    end;

    theorem :: MESFUN11:27

    for X,Y be non empty set, f1,f2 be PartFunc of X, ExtREAL st ( dom f1) c= Y & f2 = (Y --> 0 ) holds (f1 + f2) = f1 & (f1 - f2) = f1 & (f2 - f1) = ( - f1)

    proof

      let X,Y be non empty set, f1,f2 be PartFunc of X, ExtREAL ;

      assume that

       A1: ( dom f1) c= Y and

       A2: f2 = (Y --> 0 );

      

       A3: ( dom f2) = Y by A2, FUNCOP_1: 13;

      f2 is without-infty without+infty by A2, Th21;

      then

       A4: ( dom (f1 + f2)) = (( dom f1) /\ ( dom f2)) & ( dom (f1 - f2)) = (( dom f1) /\ ( dom f2)) & ( dom (f2 - f1)) = (( dom f1) /\ ( dom f2)) by Th23;

      then

       A5: ( dom (f1 + f2)) = ( dom f1) & ( dom (f1 - f2)) = ( dom f1) & ( dom (f2 - f1)) = ( dom f1) by A1, A3, XBOOLE_1: 28;

      then

       A6: ( dom ( - f1)) = ( dom (f2 - f1)) by MESFUNC1:def 7;

      now

        let x be Element of X;

        assume

         A7: x in ( dom (f1 + f2));

        then

         A8: (f2 . x) = 0 by A1, A2, A5, FUNCOP_1: 7;

        ((f1 + f2) . x) = ((f1 . x) + (f2 . x)) by A7, MESFUNC1:def 3;

        hence ((f1 + f2) . x) = (f1 . x) by A8, XXREAL_3: 4;

      end;

      hence (f1 + f2) = f1 by A4, A1, A3, XBOOLE_1: 28, PARTFUN1: 5;

      now

        let x be Element of X;

        assume

         A9: x in ( dom (f1 - f2));

        then

         A10: (f2 . x) = 0 by A1, A2, A5, FUNCOP_1: 7;

        ((f1 - f2) . x) = ((f1 . x) - (f2 . x)) by A9, MESFUNC1:def 4;

        hence ((f1 - f2) . x) = (f1 . x) by A10, XXREAL_3: 15;

      end;

      hence (f1 - f2) = f1 by A4, A1, A3, XBOOLE_1: 28, PARTFUN1: 5;

      now

        let x be Element of X;

        assume

         A11: x in ( dom (f2 - f1));

        then

         A12: (f2 . x) = 0 by A1, A2, A5, FUNCOP_1: 7;

        ((f2 - f1) . x) = ((f2 . x) - (f1 . x)) by A11, MESFUNC1:def 4

        .= (( - (f1 . x)) + (f2 . x)) by XXREAL_3:def 4

        .= ( - (f1 . x)) by A12, XXREAL_3: 4;

        hence ((f2 - f1) . x) = (( - f1) . x) by A11, A6, MESFUNC1:def 7;

      end;

      hence (f2 - f1) = ( - f1) by A6, PARTFUN1: 5;

    end;

    theorem :: MESFUN11:28

    

     Th28: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f,g be PartFunc of X, ExtREAL st f is_simple_func_in S & g is_simple_func_in S holds (f + g) is_simple_func_in S

    proof

      let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f,g be PartFunc of X, ExtREAL such that

       A1: f is_simple_func_in S and

       A4: g is_simple_func_in S;

      g is real-valued by A4, MESFUNC2:def 4;

      then

       A8: ( dom (f + g)) = (( dom f) /\ ( dom g)) by MESFUNC2: 2;

      consider F be Finite_Sep_Sequence of S, a be FinSequence of ExtREAL such that

       A10: (F,a) are_Re-presentation_of f by A1, MESFUNC3: 12;

      consider G be Finite_Sep_Sequence of S, b be FinSequence of ExtREAL such that

       A9: (G,b) are_Re-presentation_of g by A4, MESFUNC3: 12;

      set la = ( len a);

      set lb = ( len b);

      

       A11: ( dom F) = ( dom a) & ( dom G) = ( dom b) by A9, A10, MESFUNC3:def 1;

      deffunc FG1( Nat) = ((F . ((($1 -' 1) div lb) + 1)) /\ (G . ((($1 -' 1) mod lb) + 1)));

      consider FG be FinSequence such that

       A12: ( len FG) = (la * lb) and

       A13: for k be Nat st k in ( dom FG) holds (FG . k) = FG1(k) from FINSEQ_1:sch 2;

      

       A14: ( dom FG) = ( Seg (la * lb)) by A12, FINSEQ_1:def 3;

      now

        let k be Nat;

        assume k in ( dom FG);

        then (FG . k) = ((F . (((k -' 1) div lb) + 1)) /\ (G . (((k -' 1) mod lb) + 1))) by A13;

        hence (FG . k) in S;

      end;

      then

      reconsider FG as FinSequence of S by FINSEQ_2: 12;

      for k,l be Nat st k in ( dom FG) & l in ( dom FG) & k <> l holds (FG . k) misses (FG . l)

      proof

        let k,l be Nat;

        assume that

         A25: k in ( dom FG) and

         A26: l in ( dom FG) and

         A27: k <> l;

        set m = (((l -' 1) mod lb) + 1);

        set n = (((l -' 1) div lb) + 1);

        set j = (((k -' 1) mod lb) + 1);

        set i = (((k -' 1) div lb) + 1);

        

         A29: (FG . k) = ((F . i) /\ (G . j)) by A13, A25;

        

         A30: k in ( Seg (la * lb)) by A12, A25, FINSEQ_1:def 3;

        

         A31: 1 <= k & k <= (la * lb) & 1 <= l & l <= (la * lb) by A12, A25, A26, FINSEQ_3: 25;

        then

         A33: lb divides (la * lb) & 1 <= (la * lb) by NAT_D:def 3, XXREAL_0: 2;

        

         A34: lb <> 0 by A30;

        then lb >= 1 by NAT_1: 14;

        then

         A35: (((la * lb) -' 1) div lb) = (((la * lb) div lb) - 1) by A33, NAT_2: 15;

        (k -' 1) <= ((la * lb) -' 1) by A31, NAT_D: 42;

        then ((k -' 1) div lb) <= (((la * lb) div lb) - 1) by A35, NAT_2: 24;

        then i <= ((la * lb) div lb) by XREAL_1: 19;

        then i <= la by A34, NAT_D: 18;

        then

         A37: i in ( dom F) by A11, NAT_1: 11, FINSEQ_3: 25;

        m <= lb & j <= lb by A34, NAT_D: 1, NAT_1: 13;

        then

         A42: m in ( dom G) & j in ( dom G) by A11, NAT_1: 11, FINSEQ_3: 25;

        (l -' 1) <= ((la * lb) -' 1) by A31, NAT_D: 42;

        then ((l -' 1) div lb) <= (((la * lb) div lb) - 1) by A35, NAT_2: 24;

        then n <= ((la * lb) div lb) by XREAL_1: 19;

        then n <= la by A34, NAT_D: 18;

        then

         A44: n in ( dom F) by A11, NAT_1: 11, FINSEQ_3: 25;

        ((l -' 1) + 1) = ((((n - 1) * lb) + (m - 1)) + 1) by A34, NAT_D: 2;

        then

         A40: ((l - 1) + 1) = (((n - 1) * lb) + m) by A31, XREAL_1: 233;

        ((k -' 1) + 1) = ((((i - 1) * lb) + (j - 1)) + 1) by A34, NAT_D: 2;

        then

         A41: ((k - 1) + 1) = (((i - 1) * lb) + j) by A31, XREAL_1: 233;

        per cases by A27, A40, A41;

          suppose i <> n;

          then

           A45: (F . i) misses (F . n) by A37, A44, MESFUNC3: 4;

          ((FG . k) /\ (FG . l)) = (((F . i) /\ (G . j)) /\ ((F . n) /\ (G . m))) by A13, A26, A29

          .= ((F . i) /\ ((G . j) /\ ((F . n) /\ (G . m)))) by XBOOLE_1: 16

          .= ((F . i) /\ ((F . n) /\ ((G . j) /\ (G . m)))) by XBOOLE_1: 16

          .= (((F . i) /\ (F . n)) /\ ((G . j) /\ (G . m))) by XBOOLE_1: 16

          .= {} by A45;

          hence thesis;

        end;

          suppose j <> m;

          then

           A46: (G . j) misses (G . m) by A42, MESFUNC3: 4;

          ((FG . k) /\ (FG . l)) = (((F . i) /\ (G . j)) /\ ((F . n) /\ (G . m))) by A13, A26, A29

          .= ((F . i) /\ ((G . j) /\ ((F . n) /\ (G . m)))) by XBOOLE_1: 16

          .= ((F . i) /\ ((F . n) /\ ((G . j) /\ (G . m)))) by XBOOLE_1: 16

          .= {} by A46;

          hence thesis;

        end;

      end;

      then

      reconsider FG as Finite_Sep_Sequence of S by MESFUNC3: 4;

      

       A51: ( dom f) = ( union ( rng F)) by A10, MESFUNC3:def 1;

      

       A70: ( dom g) = ( union ( rng G)) by A9, MESFUNC3:def 1;

      

       A71: ( dom (f + g)) = ( union ( rng FG))

      proof

        thus ( dom (f + g)) c= ( union ( rng FG))

        proof

          let z be object;

          assume z in ( dom (f + g));

          then

           A72: z in ( dom f) & z in ( dom g) by A8, XBOOLE_0:def 4;

          then

          consider Y be set such that

           A73: z in Y and

           A74: Y in ( rng F) by A51, TARSKI:def 4;

          consider Z be set such that

           A75: z in Z and

           A76: Z in ( rng G) by A70, A72, TARSKI:def 4;

          consider j be object such that

           A77: j in ( dom G) and

           A78: Z = (G . j) by A76, FUNCT_1:def 3;

          reconsider j as Element of NAT by A77;

          consider j9 be Nat such that

           A81: j = (1 + j9) by A77, Lm2, FINSEQ_3: 25;

          consider i be object such that

           A82: i in ( dom F) and

           A83: Y = (F . i) by A74, FUNCT_1:def 3;

          reconsider i as Element of NAT by A82;

          consider i9 be Nat such that

           A85: i = (1 + i9) by A82, Lm2, FINSEQ_3: 25;

          

           A80: 1 <= j & j <= lb by A11, A77, FINSEQ_3: 25;

          then

           A87: j9 < lb by A81, NAT_1: 13;

          reconsider k = (((i - 1) * lb) + j) as Nat by A85;

          

           A88: k >= ( 0 + j) by A85, XREAL_1: 6;

          

          then

           A89: (k -' 1) = (k - 1) by A80, XREAL_1: 233, XXREAL_0: 2

          .= ((i9 * lb) + j9) by A85, A81;

          then

           A90: i = (((k -' 1) div lb) + 1) by A85, A87, NAT_D:def 1;

          i <= la by A11, A82, FINSEQ_3: 25;

          then (i - 1) <= (la - 1) by XREAL_1: 9;

          then ((i - 1) * lb) <= ((la - 1) * lb) by XREAL_1: 64;

          then

           A91: k <= (((la - 1) * lb) + j) by XREAL_1: 6;

          (((la - 1) * lb) + j) <= (((la - 1) * lb) + lb) by A80, XREAL_1: 6;

          then

           A92: k <= (la * lb) by A91, XXREAL_0: 2;

          

           B1: k >= 1 by A80, A88, XXREAL_0: 2;

          then

           A93: k in ( Seg (la * lb)) by A92;

          k in ( dom FG) by A12, B1, A92, FINSEQ_3: 25;

          then

           A94: (FG . k) in ( rng FG) by FUNCT_1:def 3;

          

           A95: j = (((k -' 1) mod lb) + 1) by A81, A89, A87, NAT_D:def 2;

          z in ((F . i) /\ (G . j)) by A73, A83, A75, A78, XBOOLE_0:def 4;

          then z in (FG . k) by A13, A14, A90, A95, A93;

          hence thesis by A94, TARSKI:def 4;

        end;

        let z be object;

        assume z in ( union ( rng FG));

        then

        consider Y be set such that

         A96: z in Y and

         A97: Y in ( rng FG) by TARSKI:def 4;

        consider k be object such that

         A98: k in ( dom FG) and

         A99: Y = (FG . k) by A97, FUNCT_1:def 3;

        reconsider k as Element of NAT by A98;

        set j = (((k -' 1) mod lb) + 1);

        set i = (((k -' 1) div lb) + 1);

        (FG . k) = ((F . i) /\ (G . j)) by A13, A98;

        then

         A100: z in (F . i) & z in (G . j) by A96, A99, XBOOLE_0:def 4;

        

         A102: 1 <= k & k <= (la * lb) by A12, A98, FINSEQ_3: 25;

        

         A103: lb <> 0 by A102;

        then

         A104: lb >= 1 by NAT_1: 14;

        lb divides (la * lb) & 1 <= (la * lb) by A102, NAT_D:def 3, XXREAL_0: 2;

        then

         A105: (((la * lb) -' 1) div lb) = (((la * lb) div lb) - 1) by A104, NAT_2: 15;

        

         A106: ((la * lb) div lb) = la by A103, NAT_D: 18;

        (k -' 1) <= ((la * lb) -' 1) by A102, NAT_D: 42;

        then ((k -' 1) div lb) <= (((la * lb) div lb) - 1) by A105, NAT_2: 24;

        then i <= ((la * lb) div lb) by XREAL_1: 19;

        then i in ( dom F) by A11, A106, NAT_1: 11, FINSEQ_3: 25;

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

        then

         a107: z in ( dom f) by A51, A100, TARSKI:def 4;

        1 <= j <= lb by A103, NAT_D: 1, NAT_1: 11, NAT_1: 13;

        then j in ( dom G) by A11, FINSEQ_3: 25;

        then (G . j) in ( rng G) by FUNCT_1:def 3;

        then z in ( dom g) by A70, A100, TARSKI:def 4;

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

      end;

      

       A107: for k be Nat, x,y be Element of X st k in ( dom FG) & x in (FG . k) & y in (FG . k) holds ((f + g) . x) = ((f + g) . y)

      proof

        let k be Nat;

        let x,y be Element of X;

        assume that

         A108: k in ( dom FG) and

         A109: x in (FG . k) & y in (FG . k);

        set i = (((k -' 1) div lb) + 1);

        set j = (((k -' 1) mod lb) + 1);

        

         A110: i >= 1 & j >= 1 by NAT_1: 11;

        (FG . k) = ((F . i) /\ (G . j)) by A13, A108;

        then

         A112: x in (F . i) & x in (G . j) & y in (F . i) & y in (G . j) by A109, XBOOLE_0:def 4;

        

         A113: 1 <= k & k <= (la * lb) by A12, A108, FINSEQ_3: 25;

        then

         A115: (k -' 1) <= ((la * lb) -' 1) by NAT_D: 42;

        

         A116: lb divides (la * lb) & 1 <= (la * lb) by A113, NAT_D:def 3, XXREAL_0: 2;

        

         A117: lb <> 0 by A113;

        then lb >= 1 by NAT_1: 14;

        then (((la * lb) -' 1) div lb) = (((la * lb) div lb) - 1) by A116, NAT_2: 15;

        then ((k -' 1) div lb) <= (((la * lb) div lb) - 1) by A115, NAT_2: 24;

        then i <= ((la * lb) div lb) by XREAL_1: 19;

        then i <= la by A117, NAT_D: 18;

        then

         A119: (f . x) = (a . i) & (f . y) = (a . i) by A10, A11, A110, A112, FINSEQ_3: 25, MESFUNC3:def 1;

        

         A120: j <= lb by A117, NAT_D: 1, NAT_1: 13;

        (FG . k) in ( rng FG) by A108, FUNCT_1:def 3;

        then

         A124: x in ( dom (f + g)) & y in ( dom (f + g)) by A71, A109, TARSKI:def 4;

        

        hence ((f + g) . x) = ((f . x) + (g . x)) by MESFUNC1:def 3

        .= ((a . i) + (b . j)) by A9, A11, A110, A120, A112, A119, FINSEQ_3: 25, MESFUNC3:def 1

        .= ((f . y) + (g . y)) by A9, A11, A110, A120, A112, A119, FINSEQ_3: 25, MESFUNC3:def 1

        .= ((f + g) . y) by A124, MESFUNC1:def 3;

      end;

      now

        let x be Element of X;

        assume

         A188: x in ( dom (f + g));

        then |.((f + g) . x).| = |.((f . x) + (g . x)).| by MESFUNC1:def 3;

        then

         A189: |.((f + g) . x).| <= ( |.(f . x).| + |.(g . x).|) by EXTREAL1: 24;

        x in ( dom f) & x in ( dom g) by A188, A8, XBOOLE_0:def 4;

        then |.(f . x).| < +infty & |.(g . x).| < +infty by A1, A4, MESFUNC2:def 1, MESFUNC2:def 4;

        then ( |.(f . x).| + |.(g . x).|) <> +infty by XXREAL_3: 16;

        hence |.((f + g) . x).| < +infty by A189, XXREAL_0: 2, XXREAL_0: 4;

      end;

      hence (f + g) is_simple_func_in S by A71, A107, MESFUNC2:def 1, MESFUNC2:def 4;

    end;

    theorem :: MESFUN11:29

    for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f,g be PartFunc of X, ExtREAL st f is_simple_func_in S & g is_simple_func_in S holds (f - g) is_simple_func_in S

    proof

      let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f,g be PartFunc of X, ExtREAL such that

       A1: f is_simple_func_in S and

       A4: g is_simple_func_in S;

      (( - 1) (#) g) is_simple_func_in S by A4, MESFUNC5: 39;

      then ( - g) is_simple_func_in S by MESFUNC2: 9;

      then (f + ( - g)) is_simple_func_in S by A1, Th28;

      then ( - (g - f)) is_simple_func_in S by MEASUR11: 64;

      hence (f - g) is_simple_func_in S by MEASUR11: 64;

    end;

    theorem :: MESFUN11:30

    

     Th30: for X be non empty set, S be SigmaField of X, f be PartFunc of X, ExtREAL st f is_simple_func_in S holds ( - f) is_simple_func_in S

    proof

      let X be non empty set, S be SigmaField of X, f be PartFunc of X, ExtREAL ;

      assume

       A1: f is_simple_func_in S;

      ( - f) = (( - 1) (#) f) by MESFUNC2: 9;

      hence ( - f) is_simple_func_in S by A1, MESFUNC5: 39;

    end;

    theorem :: MESFUN11:31

    for X be non empty set, f be nonnegative PartFunc of X, ExtREAL holds f = ( max+ f)

    proof

      let X be non empty set, f be nonnegative PartFunc of X, ExtREAL ;

      

       b3: ( dom f) = ( dom ( max+ f)) by MESFUNC2:def 2;

      for x be Element of X st x in ( dom f) holds (f . x) = (( max+ f) . x)

      proof

        let x be Element of X;

        assume

         b2: x in ( dom f);

        ( max ((f . x), 0 )) = (f . x) by SUPINF_2: 51, XXREAL_0:def 10;

        hence (f . x) = (( max+ f) . x) by b2, b3, MESFUNC2:def 2;

      end;

      hence f = ( max+ f) by b3, PARTFUN1: 5;

    end;

    theorem :: MESFUN11:32

    

     Th32: for X be non empty set, f be nonpositive PartFunc of X, ExtREAL holds f = ( - ( max- f))

    proof

      let X be non empty set, f be nonpositive PartFunc of X, ExtREAL ;

      

       b1: ( dom f) = ( dom ( max- f)) by MESFUNC2:def 3

      .= ( dom ( - ( max- f))) by MESFUNC1:def 7;

      

       b3: ( dom f) = ( dom ( max+ f)) by MESFUNC2:def 2;

      for x be Element of X st x in ( dom f) holds (f . x) = (( - ( max- f)) . x)

      proof

        let x be Element of X;

        assume

         b2: x in ( dom f);

        ( max ((f . x), 0 )) = 0 by MESFUNC5: 8, XXREAL_0:def 10;

        then (( max+ f) . x) = 0 by b2, b3, MESFUNC2:def 2;

        then (( max- f) . x) = ( - (f . x)) by b2, MESFUNC2: 20;

        then (f . x) = ( - (( max- f) . x));

        hence (f . x) = (( - ( max- f)) . x) by b1, b2, MESFUNC1:def 7;

      end;

      hence f = ( - ( max- f)) by b1, PARTFUN1: 5;

    end;

    theorem :: MESFUN11:33

    

     Th33: for C be non empty set, f be PartFunc of C, ExtREAL , c be Real st c <= 0 holds ( max+ (c (#) f)) = (( - c) (#) ( max- f)) & ( max- (c (#) f)) = (( - c) (#) ( max+ f))

    proof

      let C be non empty set;

      let f be PartFunc of C, ExtREAL ;

      let c be Real;

      assume

       A1: c <= 0 ;

      

       A2: ( dom ( max+ (c (#) f))) = ( dom (c (#) f)) by MESFUNC2:def 2

      .= ( dom f) by MESFUNC1:def 6

      .= ( dom ( max- f)) by MESFUNC2:def 3

      .= ( dom (( - c) (#) ( max- f))) by MESFUNC1:def 6;

      for x be Element of C st x in ( dom ( max+ (c (#) f))) holds (( max+ (c (#) f)) . x) = ((( - c) (#) ( max- f)) . x)

      proof

        let x be Element of C;

        assume

         A3: x in ( dom ( max+ (c (#) f)));

        then

         A4: x in ( dom (c (#) f)) by MESFUNC2:def 2;

        then x in ( dom f) by MESFUNC1:def 6;

        then

         A5: x in ( dom ( max- f)) by MESFUNC2:def 3;

        

         A6: (( max+ (c (#) f)) . x) = ( max (((c (#) f) . x), 0 )) by A3, MESFUNC2:def 2

        .= ( max ((c * (f . x)), 0 )) by A4, MESFUNC1:def 6;

        

         B1: ((( - c) (#) ( max- f)) . x) = (( - c) * (( max- f) . x)) by A2, A3, MESFUNC1:def 6

        .= (( - c) * ( max (( - (f . x)), 0 ))) by A5, MESFUNC2:def 3;

        per cases ;

          suppose (f . x) >= 0 ;

          then (( max+ (c (#) f)) . x) = 0 & ( max (( - (f . x)), 0 )) = 0 by A1, A6, XXREAL_0:def 10;

          hence thesis by B1;

        end;

          suppose

           D1: (f . x) < 0 ;

          then

           B2: (( max+ (c (#) f)) . x) = (c * (f . x)) & ( max (( - (f . x)), 0 )) = ( - (f . x)) by A1, A6, XXREAL_0:def 10;

          per cases by D1, XXREAL_0: 14;

            suppose

             E1: (f . x) = -infty ;

            per cases by A1;

              suppose c = 0 ;

              then (( max+ (c (#) f)) . x) = 0 & ((( - c) (#) ( max- f)) . x) = 0 by B1, A6, XXREAL_0:def 10;

              hence thesis;

            end;

              suppose

               F1: c < 0 ;

              then (( - c) * ( - (f . x))) = +infty by E1, XXREAL_3: 5, XXREAL_3:def 5;

              hence thesis by B1, B2, E1, F1, XXREAL_3:def 5;

            end;

          end;

            suppose (f . x) in REAL ;

            then

            reconsider a = (f . x) as Real;

            (( - c) * ( - a)) = (( - c) * ( - (f . x)));

            

            then (( - c) * ( - (f . x))) = (c * a)

            .= (c * (f . x));

            hence thesis by B1, B2;

          end;

        end;

      end;

      hence ( max+ (c (#) f)) = (( - c) (#) ( max- f)) by A2, PARTFUN1: 5;

      

       A7: ( dom ( max- (c (#) f))) = ( dom (c (#) f)) by MESFUNC2:def 3

      .= ( dom f) by MESFUNC1:def 6

      .= ( dom ( max+ f)) by MESFUNC2:def 2

      .= ( dom (( - c) (#) ( max+ f))) by MESFUNC1:def 6;

      for x be Element of C st x in ( dom ( max- (c (#) f))) holds (( max- (c (#) f)) . x) = ((( - c) (#) ( max+ f)) . x)

      proof

        let x be Element of C;

        assume

         A8: x in ( dom ( max- (c (#) f)));

        then

         A9: x in ( dom (c (#) f)) by MESFUNC2:def 3;

        then x in ( dom f) by MESFUNC1:def 6;

        then

         A10: x in ( dom ( max+ f)) by MESFUNC2:def 2;

        

         A11: (( max- (c (#) f)) . x) = ( max (( - ((c (#) f) . x)), 0 )) by A8, MESFUNC2:def 3

        .= ( max (( - (c * (f . x))), 0 )) by A9, MESFUNC1:def 6;

        

         A12: ((( - c) (#) ( max+ f)) . x) = (( - c) * (( max+ f) . x)) by A7, A8, MESFUNC1:def 6

        .= (( - c) * ( max ((f . x), 0 ))) by A10, MESFUNC2:def 2

        .= ( max ((( - c) * (f . x)),(( - c) * 0 qua ExtReal))) by A1, MESFUNC5: 6

        .= ( max ((( - c) * (f . x)), 0 ));

        ( - (c * (f . x))) = (( - c) * (f . x))

        proof

          per cases by XXREAL_0: 14;

            suppose

             E1: (f . x) = +infty ;

            per cases by A1;

              suppose c = 0 ;

              then (c * (f . x)) = 0 & (( - c) * (f . x)) = 0 ;

              hence ( - (c * (f . x))) = (( - c) * (f . x));

            end;

              suppose

               E2: c < 0 ;

              then (c * (f . x)) = -infty by E1, XXREAL_3:def 5;

              hence ( - (c * (f . x))) = (( - c) * (f . x)) by E1, E2, XXREAL_3: 5, XXREAL_3:def 5;

            end;

          end;

            suppose

             E1: (f . x) = -infty ;

            per cases by A1;

              suppose c = 0 ;

              then (c * (f . x)) = 0 & (( - c) * (f . x)) = 0 ;

              hence ( - (c * (f . x))) = (( - c) * (f . x));

            end;

              suppose

               E2: c < 0 ;

              then (c * (f . x)) = +infty by E1, XXREAL_3:def 5;

              hence ( - (c * (f . x))) = (( - c) * (f . x)) by E1, E2, XXREAL_3: 6, XXREAL_3:def 5;

            end;

          end;

            suppose (f . x) in REAL ;

            then

            reconsider a = (f . x) as Real;

            (( - c) * a) = (( - c) * (f . x));

            then (( - c) * (f . x)) = ( - (c * a));

            hence ( - (c * (f . x))) = (( - c) * (f . x));

          end;

        end;

        hence thesis by A11, A12;

      end;

      hence thesis by A7, PARTFUN1: 5;

    end;

    theorem :: MESFUN11:34

    

     Th34: for X be non empty set, f be PartFunc of X, ExtREAL holds ( max+ f) = ( max- ( - f))

    proof

      let X be non empty set, f be PartFunc of X, ExtREAL ;

      ( - f) = (( - 1) (#) f) by MESFUNC2: 9;

      then ( max- ( - f)) = (( - ( - 1)) (#) ( max+ f)) by Th33;

      hence thesis by MESFUNC2: 1;

    end;

    theorem :: MESFUN11:35

    

     Th35: for X be non empty set, f be PartFunc of X, ExtREAL , r1,r2 be Real holds (r1 (#) (r2 (#) f)) = ((r1 * r2) (#) f)

    proof

      let X be non empty set, f be PartFunc of X, ExtREAL , r1,r2 be Real;

      

       A1: ( dom (r1 (#) (r2 (#) f))) = ( dom (r2 (#) f)) by MESFUNC1:def 6;

      then

       A2: ( dom (r1 (#) (r2 (#) f))) = ( dom f) by MESFUNC1:def 6;

      

       A3: ( dom ((r1 * r2) (#) f)) = ( dom f) by MESFUNC1:def 6;

      for x be Element of X st x in ( dom (r1 (#) (r2 (#) f))) holds ((r1 (#) (r2 (#) f)) . x) = (((r1 * r2) (#) f) . x)

      proof

        let x be Element of X;

        assume

         A4: x in ( dom (r1 (#) (r2 (#) f)));

        then ((r1 (#) (r2 (#) f)) . x) = (r1 * ((r2 (#) f) . x)) by MESFUNC1:def 6;

        then

         A5: ((r1 (#) (r2 (#) f)) . x) = (r1 * (r2 * (f . x))) by A1, A4, MESFUNC1:def 6;

        (((r1 * r2) (#) f) . x) = ((r1 * r2) * (f . x)) by A2, A3, A4, MESFUNC1:def 6;

        hence thesis by A5, XXREAL_3: 66;

      end;

      hence (r1 (#) (r2 (#) f)) = ((r1 * r2) (#) f) by A2, A3, PARTFUN1: 5;

    end;

    theorem :: MESFUN11:36

    

     Th36: for X be non empty set, f,g be PartFunc of X, ExtREAL st f = ( - g) holds g = ( - f)

    proof

      let X be non empty set, f,g be PartFunc of X, ExtREAL ;

      assume f = ( - g);

      then f = (( - 1) (#) g) by MESFUNC2: 9;

      then ( - f) = (( - 1) (#) (( - 1) (#) g)) by MESFUNC2: 9;

      then ( - f) = ((( - 1) * ( - 1)) (#) g) by Th35;

      hence g = ( - f) by MESFUNC2: 1;

    end;

    definition

      let X be non empty set;

      let F be Functional_Sequence of X, ExtREAL ;

      let r be Real;

      :: MESFUN11:def1

      func r (#) F -> Functional_Sequence of X, ExtREAL means

      : Def1: for n be Nat holds (it . n) = (r (#) (F . n));

      existence

      proof

        deffunc U( Nat) = (r (#) (F . $1));

        thus ex f be Functional_Sequence of X, ExtREAL st for n be Nat holds (f . n) = U(n) from SEQFUNC:sch 1;

      end;

      uniqueness

      proof

        let H1,H2 be Functional_Sequence of X, ExtREAL such that

         A1: for n be Nat holds (H1 . n) = (r (#) (F . n)) and

         A2: for n be Nat holds (H2 . n) = (r (#) (F . n));

        now

          let n be Element of NAT ;

          (H1 . n) = (r (#) (F . n)) by A1;

          hence (H1 . n) = (H2 . n) by A2;

        end;

        hence H1 = H2 by FUNCT_2: 63;

      end;

    end

    definition

      let X be non empty set;

      let F be Functional_Sequence of X, ExtREAL ;

      :: MESFUN11:def2

      func - F -> Functional_Sequence of X, ExtREAL equals (( - 1) (#) F);

      correctness ;

    end

    theorem :: MESFUN11:37

    

     Th37: for X be non empty set, F be Functional_Sequence of X, ExtREAL , n be Nat holds (( - F) . n) = ( - (F . n))

    proof

      let X be non empty set, F be Functional_Sequence of X, ExtREAL , n be Nat;

      

      thus (( - F) . n) = (( - 1) (#) (F . n)) by Def1

      .= ( - (F . n)) by MESFUNC2: 9;

    end;

    theorem :: MESFUN11:38

    

     Th38: for X be non empty set, F be Functional_Sequence of X, ExtREAL , x be Element of X holds (( - F) # x) = ( - (F # x))

    proof

      let X be non empty set, F be Functional_Sequence of X, ExtREAL , x be Element of X;

      now

        let n be Element of NAT ;

        

         A1: ( dom ( - (F # x))) = NAT by FUNCT_2:def 1;

        

         A2: ((( - F) # x) . n) = ((( - F) . n) . x) by MESFUNC5:def 13

        .= (( - (F . n)) . x) by Th37;

        

         A3: (( - (F # x)) . n) = ( - ((F # x) . n)) by A1, MESFUNC1:def 7

        .= ( - ((F . n) . x)) by MESFUNC5:def 13;

        

         A4: ( dom (F . n)) = ( dom ( - (F . n))) by MESFUNC1:def 7;

        per cases ;

          suppose x in ( dom (F . n));

          hence ((( - F) # x) . n) = (( - (F # x)) . n) by A3, A2, A4, MESFUNC1:def 7;

        end;

          suppose

           A5: not x in ( dom (F . n));

          then

           A6: not x in ( dom ( - (F . n))) by MESFUNC1:def 7;

          (( - (F # x)) . n) = ( - 0 ) by A3, A5, FUNCT_1:def 2;

          hence ((( - F) # x) . n) = (( - (F # x)) . n) by A6, A2, FUNCT_1:def 2;

        end;

      end;

      hence (( - F) # x) = ( - (F # x)) by FUNCT_2:def 8;

    end;

    theorem :: MESFUN11:39

    

     Th39: for X be non empty set, F be Functional_Sequence of X, ExtREAL , x be Element of X holds ((F # x) is convergent_to_+infty iff (( - F) # x) is convergent_to_-infty) & ((F # x) is convergent_to_-infty iff (( - F) # x) is convergent_to_+infty) & ((F # x) is convergent_to_finite_number iff (( - F) # x) is convergent_to_finite_number) & ((F # x) is convergent iff (( - F) # x) is convergent) & ((F # x) is convergent implies ( lim (( - F) # x)) = ( - ( lim (F # x))))

    proof

      let X be non empty set, F be Functional_Sequence of X, ExtREAL , x be Element of X;

      

       A1: (F # x) is convergent_to_+infty implies ( - (F # x)) is convergent_to_-infty by DBLSEQ_3: 17;

      ( - (F # x)) is convergent_to_-infty implies ( - ( - (F # x))) is convergent_to_+infty by DBLSEQ_3: 17;

      hence

       A2: (F # x) is convergent_to_+infty iff (( - F) # x) is convergent_to_-infty by A1, DBLSEQ_3: 2, Th38;

      

       A3: (F # x) is convergent_to_-infty implies ( - (F # x)) is convergent_to_+infty by DBLSEQ_3: 17;

      ( - (F # x)) is convergent_to_+infty implies ( - ( - (F # x))) is convergent_to_-infty by DBLSEQ_3: 17;

      hence

       A4: (F # x) is convergent_to_-infty iff (( - F) # x) is convergent_to_+infty by A3, DBLSEQ_3: 2, Th38;

      

       A5: (F # x) is convergent_to_finite_number implies ( - (F # x)) is convergent_to_finite_number by DBLSEQ_3: 17;

      ( - (F # x)) is convergent_to_finite_number implies ( - ( - (F # x))) is convergent_to_finite_number by DBLSEQ_3: 17;

      hence

       A6: (F # x) is convergent_to_finite_number iff (( - F) # x) is convergent_to_finite_number by A5, Th38, DBLSEQ_3: 2;

      thus (F # x) is convergent iff (( - F) # x) is convergent by A2, A4, A6, MESFUNC5:def 11;

      hereby

        assume (F # x) is convergent;

        then ( lim ( - (F # x))) = ( - ( lim (F # x))) by DBLSEQ_3: 17;

        hence ( lim (( - F) # x)) = ( - ( lim (F # x))) by Th38;

      end;

    end;

    theorem :: MESFUN11:40

    

     Th40: for X be non empty set, F be Functional_Sequence of X, ExtREAL st F is with_the_same_dom holds ( - F) is with_the_same_dom

    proof

      let X be non empty set, F be Functional_Sequence of X, ExtREAL ;

      assume

       A1: F is with_the_same_dom;

      now

        let n,m be Nat;

        (( - F) . n) = ( - (F . n)) & (( - F) . m) = ( - (F . m)) by Th37;

        then ( dom (( - F) . n)) = ( dom (F . n)) & ( dom (( - F) . m)) = ( dom (F . m)) by MESFUNC1:def 7;

        hence ( dom (( - F) . n)) = ( dom (( - F) . m)) by A1, MESFUNC8:def 2;

      end;

      hence ( - F) is with_the_same_dom by MESFUNC8:def 2;

    end;

    theorem :: MESFUN11:41

    

     Th41: for X be non empty set, F be Functional_Sequence of X, ExtREAL st F is additive holds ( - F) is additive

    proof

      let X be non empty set, F be Functional_Sequence of X, ExtREAL ;

      assume

       A1: F is additive;

      now

        let n,m be Nat;

        assume n <> m;

        let x be set;

        assume x in (( dom (( - F) . n)) /\ ( dom (( - F) . m)));

        then x in (( dom ( - (F . n))) /\ ( dom (( - F) . m))) by Th37;

        then

         A3: x in (( dom ( - (F . n))) /\ ( dom ( - (F . m)))) by Th37;

        then x in ( dom ( - (F . n))) & x in ( dom ( - (F . m))) by XBOOLE_0:def 4;

        then (( - (F . n)) . x) = ( - ((F . n) . x)) & (( - (F . m)) . x) = ( - ((F . m) . x)) by MESFUNC1:def 7;

        then

         A4: ((( - F) . n) . x) = ( - ((F . n) . x)) & ((( - F) . m) . x) = ( - ((F . m) . x)) by Th37;

        x in (( dom (F . n)) /\ ( dom ( - (F . m)))) by A3, MESFUNC1:def 7;

        then x in (( dom (F . n)) /\ ( dom (F . m))) by MESFUNC1:def 7;

        hence ((( - F) . n) . x) <> +infty or ((( - F) . m) . x) <> -infty by A4, XXREAL_3: 6, A1, MESFUNC9:def 5;

      end;

      hence ( - F) is additive by MESFUNC9:def 5;

    end;

    theorem :: MESFUN11:42

    

     Th42: for X be non empty set, F be Functional_Sequence of X, ExtREAL , n be Nat holds (( Partial_Sums ( - F)) . n) = (( - ( Partial_Sums F)) . n)

    proof

      let X be non empty set, F be Functional_Sequence of X, ExtREAL , n be Nat;

      defpred P[ Nat] means (( Partial_Sums ( - F)) . $1) = (( - ( Partial_Sums F)) . $1);

      (( Partial_Sums ( - F)) . 0 ) = (( - F) . 0 ) by MESFUNC9:def 4

      .= ( - (F . 0 )) by Th37

      .= ( - (( Partial_Sums F) . 0 )) by MESFUNC9:def 4;

      then

       A1: P[ 0 ] by Th37;

      

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

      proof

        let k be Nat;

        assume

         A3: P[k];

        (( Partial_Sums ( - F)) . (k + 1)) = ((( Partial_Sums ( - F)) . k) + (( - F) . (k + 1))) by MESFUNC9:def 4

        .= ((( - ( Partial_Sums F)) . k) + ( - (F . (k + 1)))) by A3, Th37

        .= (( - (( Partial_Sums F) . k)) + ( - (F . (k + 1)))) by Th37

        .= ( - ((( Partial_Sums F) . k) + (F . (k + 1)))) by MEASUR11: 64

        .= ( - (( Partial_Sums F) . (k + 1))) by MESFUNC9:def 4;

        hence P[(k + 1)] by Th37;

      end;

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

      hence (( Partial_Sums ( - F)) . n) = (( - ( Partial_Sums F)) . n);

    end;

    theorem :: MESFUN11:43

    

     Th43: for seq be ExtREAL_sequence, n be Nat holds (( Partial_Sums ( - seq)) . n) = ( - (( Partial_Sums seq) . n))

    proof

      let seq be ExtREAL_sequence, n be Nat;

      defpred P[ Nat] means (( Partial_Sums ( - seq)) . $1) = ( - (( Partial_Sums seq) . $1));

      

       A1: ( dom ( - seq)) = NAT by FUNCT_2:def 1;

      (( Partial_Sums ( - seq)) . 0 ) = (( - seq) . 0 ) by MESFUNC9:def 1

      .= ( - (seq . 0 )) by A1, MESFUNC1:def 7;

      then

       A3: P[ 0 ] by MESFUNC9:def 1;

      

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

      proof

        let k be Nat;

        assume

         A5: P[k];

        (( Partial_Sums ( - seq)) . (k + 1)) = ((( Partial_Sums ( - seq)) . k) + (( - seq) . (k + 1))) by MESFUNC9:def 1

        .= (( - (( Partial_Sums seq) . k)) + ( - (seq . (k + 1)))) by A1, A5, MESFUNC1:def 7

        .= ( - ((( Partial_Sums seq) . k) + (seq . (k + 1)))) by XXREAL_3: 9;

        hence P[(k + 1)] by MESFUNC9:def 1;

      end;

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

      hence (( Partial_Sums ( - seq)) . n) = ( - (( Partial_Sums seq) . n));

    end;

    theorem :: MESFUN11:44

    

     Th44: for seq be ExtREAL_sequence holds ( Partial_Sums ( - seq)) = ( - ( Partial_Sums seq))

    proof

      let seq be ExtREAL_sequence;

      now

        let n be Element of NAT ;

        

         A1: ( dom ( - ( Partial_Sums seq))) = NAT by FUNCT_2:def 1;

        (( Partial_Sums ( - seq)) . n) = ( - (( Partial_Sums seq) . n)) by Th43;

        hence (( Partial_Sums ( - seq)) . n) = (( - ( Partial_Sums seq)) . n) by A1, MESFUNC1:def 7;

      end;

      hence ( Partial_Sums ( - seq)) = ( - ( Partial_Sums seq)) by FUNCT_2:def 8;

    end;

    theorem :: MESFUN11:45

    

     Th45: for seq be ExtREAL_sequence st seq is summable holds ( - seq) is summable

    proof

      let seq be ExtREAL_sequence;

      assume seq is summable;

      then

       A1: ( Partial_Sums seq) is convergent by MESFUNC9:def 2;

      ( Partial_Sums ( - seq)) = ( - ( Partial_Sums seq)) by Th44;

      hence ( - seq) is summable by A1, DBLSEQ_3: 17, MESFUNC9:def 2;

    end;

    theorem :: MESFUN11:46

    

     Th46: for X be non empty set, F be Functional_Sequence of X, ExtREAL st (for n be Nat holds (F . n) is without+infty) holds F is additive

    proof

      let X be non empty set, F be Functional_Sequence of X, ExtREAL ;

      assume for n be Nat holds (F . n) is without+infty;

      then for n,m be Nat st n <> m holds for x be set st x in (( dom (F . n)) /\ ( dom (F . m))) holds ((F . n) . x) <> +infty or ((F . m) . x) <> -infty by MESFUNC5:def 6;

      hence F is additive by MESFUNC9:def 5;

    end;

    theorem :: MESFUN11:47

    

     Th47: for X be non empty set, F be Functional_Sequence of X, ExtREAL st (for n be Nat holds (F . n) is without-infty) holds F is additive

    proof

      let X be non empty set, F be Functional_Sequence of X, ExtREAL ;

      assume for n be Nat holds (F . n) is without-infty;

      then for n,m be Nat st n <> m holds for x be set st x in (( dom (F . n)) /\ ( dom (F . m))) holds ((F . n) . x) <> +infty or ((F . m) . x) <> -infty by MESFUNC5:def 5;

      hence F is additive by MESFUNC9:def 5;

    end;

    theorem :: MESFUN11:48

    

     Th48: for X be non empty set, F be Functional_Sequence of X, ExtREAL , x be Element of X st (F # x) is summable holds (( - F) # x) is summable & ( Sum (( - F) # x)) = ( - ( Sum (F # x)))

    proof

      let X be non empty set, F be Functional_Sequence of X, ExtREAL , x be Element of X;

      assume

       A1: (F # x) is summable;

      then ( - (F # x)) is summable by Th45;

      hence (( - F) # x) is summable by Th38;

      

       A2: ( - (F # x)) = (( - F) # x) by Th38;

      ( Partial_Sums (F # x)) is convergent by A1, MESFUNC9:def 2;

      then ( lim ( - ( Partial_Sums (F # x)))) = ( - ( lim ( Partial_Sums (F # x)))) by DBLSEQ_3: 17;

      then ( lim ( Partial_Sums ( - (F # x)))) = ( - ( lim ( Partial_Sums (F # x)))) by Th44;

      then ( lim ( Partial_Sums (( - F) # x))) = ( - ( Sum (F # x))) by A2, MESFUNC9:def 3;

      hence ( Sum (( - F) # x)) = ( - ( Sum (F # x))) by MESFUNC9:def 3;

    end;

    theorem :: MESFUN11:49

    

     Th49: for X be non empty set, S be SigmaField of X, F be Functional_Sequence of X, ExtREAL st F is additive & F is with_the_same_dom & (for x be Element of X st x in ( dom (F . 0 )) holds (F # x) is summable) holds ( lim ( Partial_Sums ( - F))) = ( - ( lim ( Partial_Sums F)))

    proof

      let X be non empty set, S be SigmaField of X, F be Functional_Sequence of X, ExtREAL ;

      assume that

       A1: F is additive and

       A2: F is with_the_same_dom and

       A3: for x be Element of X st x in ( dom (F . 0 )) holds (F # x) is summable;

      set G = ( - F);

      for n be Element of NAT holds (( Partial_Sums G) . n) = (( - ( Partial_Sums F)) . n) by Th42;

      then

       A4: ( Partial_Sums G) = ( - ( Partial_Sums F)) by FUNCT_2:def 7;

      

       A5: ( dom ( lim ( Partial_Sums G))) = ( dom (( Partial_Sums G) . 0 )) by MESFUNC8:def 9

      .= ( dom (G . 0 )) by MESFUNC9:def 4

      .= ( dom ( - (F . 0 ))) by Th37

      .= ( dom (F . 0 )) by MESFUNC1:def 7;

      

       A6: ( dom ( - ( lim ( Partial_Sums F)))) = ( dom ( lim ( Partial_Sums F))) by MESFUNC1:def 7;

      

      then

       A7: ( dom ( - ( lim ( Partial_Sums F)))) = ( dom (( Partial_Sums F) . 0 )) by MESFUNC8:def 9

      .= ( dom (F . 0 )) by MESFUNC9:def 4;

      for x be Element of X st x in ( dom ( lim ( Partial_Sums G))) holds (( lim ( Partial_Sums G)) . x) = (( - ( lim ( Partial_Sums F))) . x)

      proof

        let x be Element of X;

        assume

         A8: x in ( dom ( lim ( Partial_Sums G)));

        then (F # x) is summable by A3, A5;

        then ( Partial_Sums (F # x)) is convergent by MESFUNC9:def 2;

        then

         A9: (( Partial_Sums F) # x) is convergent by A1, A2, A8, A5, MESFUNC9: 33;

        (( Partial_Sums G) # x) = ( - (( Partial_Sums F) # x)) by A4, Th38;

        then

         A10: ( lim (( Partial_Sums G) # x)) = ( - ( lim (( Partial_Sums F) # x))) by A9, DBLSEQ_3: 17;

        (( - ( lim ( Partial_Sums F))) . x) = ( - (( lim ( Partial_Sums F)) . x)) by A7, A5, A8, MESFUNC1:def 7;

        then (( - ( lim ( Partial_Sums F))) . x) = ( - ( lim (( Partial_Sums F) # x))) by A7, A5, A8, A6, MESFUNC8:def 9;

        hence (( lim ( Partial_Sums G)) . x) = (( - ( lim ( Partial_Sums F))) . x) by A8, A10, MESFUNC8:def 9;

      end;

      hence ( lim ( Partial_Sums G)) = ( - ( lim ( Partial_Sums F))) by A7, A5, PARTFUN1: 5;

    end;

    theorem :: MESFUN11:50

    

     Th50: for X be non empty set, S be SigmaField of X, F,G be Functional_Sequence of X, ExtREAL , E be Element of S st E c= ( dom (F . 0 )) & F is additive & F is with_the_same_dom & (for n be Nat holds (G . n) = ((F . n) | E)) holds ( lim ( Partial_Sums G)) = (( lim ( Partial_Sums F)) | E)

    proof

      let X be non empty set, S be SigmaField of X, F,G be Functional_Sequence of X, ExtREAL , E be Element of S;

      assume that

       A1: E c= ( dom (F . 0 )) and

       A2: F is additive and

       A3: F is with_the_same_dom and

       A5: for n be Nat holds (G . n) = ((F . n) | E);

      

       A6: G is additive with_the_same_dom Functional_Sequence of X, ExtREAL by A2, A3, A5, MESFUNC9: 18, MESFUNC9: 31;

      ( dom ((F . 0 ) | E)) = E by A1, RELAT_1: 62;

      then

       A8: E = ( dom (G . 0 )) by A5;

      

       A9: for x be Element of X st x in E holds (F # x) = (G # x)

      proof

        let x be Element of X;

        assume

         A10: x in E;

        for n be Element of NAT holds ((F # x) . n) = ((G # x) . n)

        proof

          let n be Element of NAT ;

          ( dom (G . n)) = E by A8, MESFUNC8:def 2, A3, A5, MESFUNC9: 18;

          then x in ( dom ((F . n) | E)) by A5, A10;

          then (((F . n) | E) . x) = ((F . n) . x) by FUNCT_1: 47;

          then

           A11: ((G . n) . x) = ((F . n) . x) by A5;

          ((F # x) . n) = ((F . n) . x) by MESFUNC5:def 13;

          hence thesis by A11, MESFUNC5:def 13;

        end;

        hence thesis by FUNCT_2:def 7;

      end;

      set E1 = ( dom (F . 0 ));

      set PF = ( Partial_Sums F);

      set PG = ( Partial_Sums G);

      

       A13: ( dom ( lim PG)) = ( dom (PG . 0 )) by MESFUNC8:def 9;

      ( dom (PF . 0 )) = E1 by A2, A3, MESFUNC9: 29;

      then

       A14: E c= ( dom ( lim PF)) by A1, MESFUNC8:def 9;

      

       A15: for x be Element of X st x in ( dom ( lim PG)) holds (( lim PG) . x) = (( lim PF) . x)

      proof

        let x be Element of X;

        set PFx = ( Partial_Sums (F # x));

        set PGx = ( Partial_Sums (G # x));

        assume

         A16: x in ( dom ( lim PG));

        then x in ( dom (G . 0 )) by A6, A13, MESFUNC9: 29;

        then x in ( dom ((F . 0 ) | E)) by A5;

        then

         A17: x in E by A1, RELAT_1: 62;

        for n be Element of NAT holds ((PG # x) . n) = ((PF # x) . n)

        proof

          let n be Element of NAT ;

          

           A18: (PGx . n) = ((PG # x) . n) by A6, A8, A17, MESFUNC9: 32;

          (PFx . n) = ((PF # x) . n) by A1, A2, A3, A17, MESFUNC9: 32;

          hence thesis by A9, A17, A18;

        end;

        then

         A19: ( lim (PG # x)) = ( lim (PF # x)) by FUNCT_2: 63;

        (( lim PG) . x) = ( lim (PG # x)) by A16, MESFUNC8:def 9;

        hence thesis by A14, A17, A19, MESFUNC8:def 9;

      end;

      

       A20: ( dom (PG . 0 )) = ( dom (G . 0 )) by A6, MESFUNC9: 29;

      

       A22: ( dom (( lim PF) | E)) = E by A14, RELAT_1: 62;

      for x be Element of X st x in ( dom (( lim PG) | E)) holds ((( lim PG) | E) . x) = ((( lim PF) | E) . x)

      proof

        let x be Element of X;

        assume

         A24: x in ( dom (( lim PG) | E));

        then ((( lim PF) | E) . x) = (( lim PF) . x) by A8, A13, A20, A22, FUNCT_1: 47;

        hence thesis by A8, A13, A20, A15, A24;

      end;

      hence thesis by A8, A20, A13, A22, PARTFUN1: 5;

    end;

    begin

    theorem :: MESFUN11:51

    for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be nonnegative PartFunc of X, ExtREAL holds ( integral' (M,( max- ( - f)))) = ( integral' (M,f))

    proof

      let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be nonnegative PartFunc of X, ExtREAL ;

      ( - f) = ( - ( max- ( - f))) by Th32;

      then f = ( - ( - ( max- ( - f)))) by Th36;

      then f = (( - 1) (#) ( - ( max- ( - f)))) by MESFUNC2: 9;

      then f = (( - 1) (#) (( - 1) (#) ( max- ( - f)))) by MESFUNC2: 9;

      then f = ((( - 1) * ( - 1)) (#) ( max- ( - f))) by Th35;

      hence ( integral' (M,( max- ( - f)))) = ( integral' (M,f)) by MESFUNC2: 1;

    end;

    theorem :: MESFUN11:52

    

     Th52: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, ExtREAL , A be Element of S st A = ( dom f) & f is A -measurable holds ( Integral (M,( - f))) = ( - ( Integral (M,f)))

    proof

      let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, ExtREAL , A be Element of S;

      assume that

       A1: A = ( dom f) and

       A2: f is A -measurable;

      set g = ( - f);

      

       A4: f = ( - g) by Th36;

      

       B6: ( dom ( max- f)) = A & ( dom ( max+ f)) = A by A1, MESFUNC2:def 2, MESFUNC2:def 3;

      

       B7: ( max- f) is A -measurable & ( max+ f) is A -measurable by A1, A2, Th10;

      

       A6: ( dom g) = A by A1, MESFUNC1:def 7;

      then

       A7: ( dom ( max+ g)) = A & ( dom ( max- g)) = A by MESFUNC2:def 2, MESFUNC2:def 3;

      g is A -measurable by A1, A2, MEASUR11: 63;

      then

       A9: ( max+ g) is A -measurable & ( max- g) is A -measurable by A6, Th10;

      

      then

       P1: ( integral+ (M,( max+ g))) = ( Integral (M,( max+ g))) by A7, Th5, MESFUNC5: 88

      .= ( Integral (M,( max- ( - g)))) by Th34

      .= ( integral+ (M,( max- f))) by A4, B6, B7, Th5, MESFUNC5: 88;

      ( integral+ (M,( max- g))) = ( Integral (M,( max- g))) by A7, A9, Th5, MESFUNC5: 88

      .= ( Integral (M,( max+ ( - g)))) by MESFUNC2: 14

      .= ( integral+ (M,( max+ f))) by A4, B6, B7, Th5, MESFUNC5: 88;

      

      then ( Integral (M,f)) = (( integral+ (M,( max- g))) - ( integral+ (M,( max+ g)))) by P1, MESFUNC5:def 16

      .= ( - (( integral+ (M,( max+ g))) - ( integral+ (M,( max- g))))) by XXREAL_3: 26;

      hence thesis by MESFUNC5:def 16;

    end;

    theorem :: MESFUN11:53

    for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be nonnegative PartFunc of X, ExtREAL , E be Element of S st E = ( dom f) & f is E -measurable holds ( Integral (M,( max- f))) = 0 & ( integral+ (M,( max- f))) = 0

    proof

      let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be nonnegative PartFunc of X, ExtREAL , E be Element of S;

      assume that

       A1: E = ( dom f) and

       A2: f is E -measurable;

      

       A3: E = ( dom ( max- f)) by A1, MESFUNC2:def 3;

      

       A4: ( max- f) is E -measurable by A1, A2, Th10;

      for x be object st x in ( dom ( max- f)) holds (( max- f) . x) = 0

      proof

        let x be object;

        assume

         A5: x in ( dom ( max- f));

        then

         A6: x in ( dom ( max+ f)) by A1, A3, MESFUNC2:def 2;

        per cases by SUPINF_2: 51;

          suppose (f . x) = 0 ;

          then (( max+ f) . x) = (f . x) by A5, MESFUNC2: 18;

          hence (( max- f) . x) = 0 by A5, MESFUNC2: 19;

        end;

          suppose (f . x) > 0 ;

          then ( max ((f . x), 0 )) = (f . x) by XXREAL_0:def 10;

          then (( max+ f) . x) = (f . x) by A6, MESFUNC2:def 2;

          hence (( max- f) . x) = 0 by A5, MESFUNC2: 19;

        end;

      end;

      

      hence ( Integral (M,( max- f))) = ( 0 * (M . ( dom ( max- f)))) by A3, MEASUR10: 27

      .= 0 ;

      hence ( integral+ (M,( max- f))) = 0 by A3, A4, Th5, MESFUNC5: 88;

    end;

    theorem :: MESFUN11:54

    for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, ExtREAL , E be Element of S st E = ( dom f) & f is E -measurable holds ( Integral (M,f)) = (( Integral (M,( max+ f))) - ( Integral (M,( max- f))))

    proof

      let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, ExtREAL , E be Element of S;

      assume that

       A1: E = ( dom f) and

       A2: f is E -measurable;

      

       A3: E = ( dom ( max+ f)) & E = ( dom ( max- f)) by A1, MESFUNC2:def 2, MESFUNC2:def 3;

      ( max+ f) is E -measurable & ( max- f) is E -measurable by A1, A2, Th10;

      then ( Integral (M,( max+ f))) = ( integral+ (M,( max+ f))) & ( Integral (M,( max- f))) = ( integral+ (M,( max- f))) by A3, Th5, MESFUNC5: 88;

      hence ( Integral (M,f)) = (( Integral (M,( max+ f))) - ( Integral (M,( max- f)))) by MESFUNC5:def 16;

    end;

    theorem :: MESFUN11:55

    

     Th55: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, ExtREAL , E be Element of S st E c= ( dom f) & f is E -measurable holds ( Integral (M,(( - f) | E))) = ( - ( Integral (M,(f | E))))

    proof

      let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, ExtREAL , E be Element of S;

      assume that

       A1: E c= ( dom f) and

       A2: f is E -measurable;

      

       A3: E = ( dom (f | E)) by A1, RELAT_1: 62;

      then

       A4: E = (( dom f) /\ E) by RELAT_1: 61;

      (( - f) | E) = ( - (f | E)) by Th3;

      hence ( Integral (M,(( - f) | E))) = ( - ( Integral (M,(f | E)))) by A3, A4, A2, MESFUNC5: 42, Th52;

    end;

    theorem :: MESFUN11:56

    

     Th56: for X be non empty set, S be SigmaField of X, f be PartFunc of X, ExtREAL st (ex A be Element of S st A = ( dom f) & f is A -measurable) & f qua ext-real-valued Function is nonpositive holds ex F be Functional_Sequence of X, ExtREAL st (for n be Nat holds (F . n) is_simple_func_in S & ( dom (F . n)) = ( dom f)) & (for n be Nat holds (F . n) is nonpositive) & (for n,m be Nat st n <= m holds for x be Element of X st x in ( dom f) holds ((F . n) . x) >= ((F . m) . x)) & for x be Element of X st x in ( dom f) holds (F # x) is convergent & ( lim (F # x)) = (f . x)

    proof

      let X be non empty set, S be SigmaField of X, f be PartFunc of X, ExtREAL ;

      assume that

       A1: ex A be Element of S st A = ( dom f) & f is A -measurable and

       A2: f qua ext-real-valued Function is nonpositive;

      set g = ( - f);

      consider A be Element of S such that

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

      

       A4: A = ( dom g) by A3, MESFUNC1:def 7;

      then

      consider G be Functional_Sequence of X, ExtREAL such that

       A6: (for n be Nat holds (G . n) is_simple_func_in S & ( dom (G . n)) = ( dom g)) & (for n be Nat holds (G . n) is nonnegative) & (for n,m be Nat st n <= m holds for x be Element of X st x in ( dom g) holds ((G . n) . x) <= ((G . m) . x)) & for x be Element of X st x in ( dom g) holds (G # x) is convergent & ( lim (G # x)) = (g . x) by A2, A3, MEASUR11: 63, MESFUNC5: 64;

      take F = ( - G);

      thus

       A8: for n be Nat holds (F . n) is_simple_func_in S & ( dom (F . n)) = ( dom f)

      proof

        let n be Nat;

        

         A9: ( dom (G . n)) = ( dom g) by A6;

        

         A10: (F . n) = ( - (G . n)) by Th37;

        hence (F . n) is_simple_func_in S by A6, Th30;

        thus ( dom (F . n)) = ( dom f) by A3, A4, A9, A10, MESFUNC1:def 7;

      end;

      thus for n be Nat holds (F . n) is nonpositive

      proof

        let n be Nat;

        

         A12: (G . n) is nonnegative by A6;

        (F . n) = ( - (G . n)) by Th37;

        hence (F . n) is nonpositive by A12;

      end;

      thus for n,m be Nat st n <= m holds for x be Element of X st x in ( dom f) holds ((F . n) . x) >= ((F . m) . x)

      proof

        let n,m be Nat;

        assume

         A14: n <= m;

        let x be Element of X;

        assume

         A15: x in ( dom f);

        ( dom (F . n)) = ( dom f) & (F . n) = ( - (G . n)) & ( dom (F . m)) = ( dom f) & (F . m) = ( - (G . m)) by A8, Th37;

        then ((F . n) . x) = ( - ((G . n) . x)) & ((F . m) . x) = ( - ((G . m) . x)) by A15, MESFUNC1:def 7;

        hence ((F . n) . x) >= ((F . m) . x) by A15, A3, A4, A6, A14, XXREAL_3: 38;

      end;

      thus for x be Element of X st x in ( dom f) holds (F # x) is convergent & ( lim (F # x)) = (f . x)

      proof

        let x be Element of X;

        assume

         A17: x in ( dom f);

        then

         A18: (G # x) is convergent & ( lim (G # x)) = (g . x) by A3, A4, A6;

        hence (F # x) is convergent by Th39;

        ( lim (F # x)) = ( - (g . x)) by A18, Th39;

        then ( lim (F # x)) = ( - ( - (f . x))) by A3, A4, A17, MESFUNC1:def 7;

        hence ( lim (F # x)) = (f . x);

      end;

    end;

    theorem :: MESFUN11:57

    

     Th57: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, E be Element of S, f be nonpositive PartFunc of X, ExtREAL st (ex A be Element of S st A = ( dom f) & f is A -measurable) holds ( Integral (M,f)) = ( - ( integral+ (M,( max- f)))) & ( Integral (M,f)) = ( - ( integral+ (M,( - f)))) & ( Integral (M,f)) = ( - ( Integral (M,( - f))))

    proof

      let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, E be Element of S, f be nonpositive PartFunc of X, ExtREAL ;

      assume ex A be Element of S st A = ( dom f) & f is A -measurable;

      then

      consider A be Element of S such that

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

      

       A3: ( dom ( max+ f)) = A by A2, MESFUNC2:def 2;

      

       A4: f = ( - ( max- f)) by Th32;

      then

       A5: ( - f) = ( max- f) by Th36;

      for x be Element of X st x in ( dom ( max+ f)) holds (( max+ f) . x) = 0

      proof

        let x be Element of X;

        assume x in ( dom ( max+ f));

        then (f . x) = ( - (( max- f) . x)) by A2, A3, A4, MESFUNC1:def 7;

        then ( - (f . x)) = (( max- f) . x);

        hence (( max+ f) . x) = 0 by MESFUNC2: 21;

      end;

      then

       A6: ( integral+ (M,( max+ f))) = 0 by A3, A2, MESFUNC2: 25, MESFUNC5: 87;

      

       A7: ( Integral (M,f)) = (( integral+ (M,( max+ f))) - ( integral+ (M,( max- f)))) by MESFUNC5:def 16

      .= (( integral+ (M,( max+ f))) + ( - ( integral+ (M,( max- f))))) by XXREAL_3:def 4;

      hence ( Integral (M,f)) = ( - ( integral+ (M,( max- f)))) by A6, XXREAL_3: 4;

      thus

       A8: ( Integral (M,f)) = ( - ( integral+ (M,( - f)))) by A5, A7, A6, XXREAL_3: 4;

      A = ( dom ( - f)) by A2, MESFUNC1:def 7;

      hence ( Integral (M,f)) = ( - ( Integral (M,( - f)))) by A8, A2, MEASUR11: 63, MESFUNC5: 88;

    end;

    theorem :: MESFUN11:58

    

     Th58: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be nonpositive PartFunc of X, ExtREAL st f is_simple_func_in S holds ( Integral (M,f)) = ( - ( integral' (M,( - f)))) & ( Integral (M,f)) = ( - ( integral' (M,( max- f))))

    proof

      let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be nonpositive PartFunc of X, ExtREAL ;

      assume

       A1: f is_simple_func_in S;

      then

      reconsider A = ( dom f) as Element of S by MESFUNC5: 37;

      

       A2: f is A -measurable by A1, MESFUNC2: 34;

      ( integral+ (M,( - f))) = ( integral' (M,( - f))) by A1, Th30, MESFUNC5: 77;

      hence

       A3: ( Integral (M,f)) = ( - ( integral' (M,( - f)))) by A2, Th57;

      f = ( - ( max- f)) by Th32;

      hence ( Integral (M,f)) = ( - ( integral' (M,( max- f)))) by A3, Th36;

    end;

    

     Lm3: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, ExtREAL , c be Real st f is_simple_func_in S & f is nonpositive & 0 <= c holds ( Integral (M,(c (#) f))) = ( - (c * ( integral' (M,( - f))))) & ( Integral (M,(c (#) f))) = (( - c) * ( integral' (M,( - f))))

    proof

      let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, ExtREAL , c be Real;

      assume that

       A1: f is_simple_func_in S and

       A2: f is nonpositive and

       A3: 0 <= c;

      

       A4: (c (#) f) is_simple_func_in S by A1, MESFUNC5: 39;

      f = ( - ( max- f)) by A2, Th32;

      then

       A6: ( - f) = ( max- f) by Th36;

      

       A7: ( - f) is_simple_func_in S by A1, Th30;

      

       A8: ( max- (c (#) f)) = (c (#) ( max- f)) by A3, MESFUNC5: 26;

      (c (#) f) is nonpositive by A2, A3, Th4;

      

      hence ( Integral (M,(c (#) f))) = ( - ( integral' (M,( max- (c (#) f))))) by A4, Th58

      .= ( - (c * ( integral' (M,( - f))))) by A3, A7, A6, A8, Th5, MESFUNC5: 66;

      hence ( Integral (M,(c (#) f))) = (( - c) * ( integral' (M,( - f)))) by XXREAL_3: 92;

    end;

    

     Lm4: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, ExtREAL , c be Real st f is_simple_func_in S & f is nonnegative & c <= 0 holds ( Integral (M,(c (#) f))) = (c * ( integral' (M,f)))

    proof

      let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, ExtREAL , c be Real;

      assume that

       A1: f is_simple_func_in S and

       A2: f is nonnegative and

       A3: c <= 0 ;

      set d = ( - c);

      

       A4: ( - f) is_simple_func_in S by A1, Th30;

      (d (#) ( - f)) = (d (#) (( - 1) (#) f)) by MESFUNC2: 9

      .= ((d * ( - 1)) (#) f) by Th35;

      then ( Integral (M,(c (#) f))) = (( - d) * ( integral' (M,( - ( - f))))) by A3, A2, A4, Lm3;

      hence ( Integral (M,(c (#) f))) = (c * ( integral' (M,f))) by DBLSEQ_3: 2;

    end;

    theorem :: MESFUN11:59

    

     Th59: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, ExtREAL , c be Real st f is_simple_func_in S & f is nonnegative holds ( Integral (M,(c (#) f))) = (c * ( integral' (M,f)))

    proof

      let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, ExtREAL , c be Real;

      assume that

       A1: f is_simple_func_in S and

       a2: f is nonnegative;

      per cases ;

        suppose

         A2: c >= 0 ;

        then

         A3: (c (#) f) is_simple_func_in S & (c (#) f) is nonnegative by A1, a2, MESFUNC5: 20, MESFUNC5: 39;

        ( integral' (M,(c (#) f))) = (c * ( integral' (M,f))) by A1, a2, A2, MESFUNC5: 66;

        hence ( Integral (M,(c (#) f))) = (c * ( integral' (M,f))) by A3, MESFUNC5: 89;

      end;

        suppose c < 0 ;

        hence ( Integral (M,(c (#) f))) = (c * ( integral' (M,f))) by A1, a2, Lm4;

      end;

    end;

    theorem :: MESFUN11:60

    for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, ExtREAL , c be Real st f is_simple_func_in S & f is nonpositive holds ( Integral (M,(c (#) f))) = (( - c) * ( integral' (M,( - f)))) & ( Integral (M,(c (#) f))) = ( - (c * ( integral' (M,( - f)))))

    proof

      let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, ExtREAL , c be Real;

      assume that

       A1: f is_simple_func_in S and

       A2: f is nonpositive;

      set d = ( - c);

      

       A3: (d (#) ( - f)) = (d (#) (( - 1) (#) f)) by MESFUNC2: 9

      .= ((d * ( - 1)) (#) f) by Th35;

      hence ( Integral (M,(c (#) f))) = (( - c) * ( integral' (M,( - f)))) by A2, A1, Th30, Th59;

      ( Integral (M,(c (#) f))) = (d * ( integral' (M,( - f)))) by A2, A1, A3, Th30, Th59;

      hence ( Integral (M,(c (#) f))) = ( - (c * ( integral' (M,( - f))))) by XXREAL_3: 92;

    end;

    theorem :: MESFUN11:61

    

     Th61: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, ExtREAL st (ex A be Element of S st A = ( dom f) & f is A -measurable) & f is nonpositive holds 0 >= ( Integral (M,f))

    proof

      let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, ExtREAL ;

      assume that

       A1: ex A be Element of S st A = ( dom f) & f is A -measurable and

       A2: f is nonpositive;

      consider A be Element of S such that

       A3: A = ( dom f) and

       a3: f is A -measurable by A1;

      

       A4: A = ( dom ( - f)) by A3, MESFUNC1:def 7;

      ( Integral (M,( - f))) >= 0 by A4, A2, A3, a3, MEASUR11: 63, MESFUNC5: 90;

      then

       A7: ( integral+ (M,( - f))) >= 0 by A4, A2, A3, a3, MEASUR11: 63, MESFUNC5: 88;

      ( Integral (M,f)) = ( - ( integral+ (M,( - f)))) by A2, A3, a3, Th57;

      hence 0 >= ( Integral (M,f)) by A7;

    end;

    theorem :: MESFUN11:62

    for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, ExtREAL , A,B,E be Element of S st E = ( dom f) & f is E -measurable & f is nonpositive & A misses B holds ( Integral (M,(f | (A \/ B)))) = (( Integral (M,(f | A))) + ( Integral (M,(f | B))))

    proof

      let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, ExtREAL , A,B,E be Element of S;

      assume that

       A1: E = ( dom f) & f is E -measurable and

       A2: f is nonpositive and

       A3: A misses B;

      set f1 = (f | (A \/ B));

      set f2 = (f | A);

      set f3 = (f | B);

      set g = ( - f);

      reconsider E1 = (E /\ (A \/ B)) as Element of S;

      

       A4: ( dom (f | (A \/ B))) = E1 by A1, RELAT_1: 61;

      

       A5: E1 = (( dom f) /\ E1) by A1, XBOOLE_1: 17, XBOOLE_1: 28;

      

       A6: f is E1 -measurable by A1, XBOOLE_1: 17, MESFUNC1: 30;

      

       A7: (f | E1) = ((f | E) | (A \/ B)) by RELAT_1: 71;

      (g | (A \/ B)) = ( - (f | (A \/ B))) by Th3;

      then

       A8: ( Integral (M,(g | (A \/ B)))) = ( - ( Integral (M,(f | (A \/ B))))) by A1, A4, A5, A6, A7, Th52, MESFUNC5: 42;

      reconsider E2 = (E /\ A) as Element of S;

      

       A9: ( dom (f | A)) = E2 by A1, RELAT_1: 61;

      

       A10: E2 = (( dom f) /\ E2) by A1, XBOOLE_1: 17, XBOOLE_1: 28;

      

       A11: f is E2 -measurable by A1, XBOOLE_1: 17, MESFUNC1: 30;

      

       A12: (f | E2) = ((f | E) | A) by RELAT_1: 71;

      (g | A) = ( - (f | A)) by Th3;

      then

       A13: ( Integral (M,(g | A))) = ( - ( Integral (M,(f | A)))) by A1, A9, A10, A11, A12, Th52, MESFUNC5: 42;

      reconsider E3 = (E /\ B) as Element of S;

      

       A14: ( dom (f | B)) = E3 by A1, RELAT_1: 61;

      

       A15: E3 = (( dom f) /\ E3) by A1, XBOOLE_1: 17, XBOOLE_1: 28;

      

       A16: f is E3 -measurable by A1, XBOOLE_1: 17, MESFUNC1: 30;

      

       A17: (f | E3) = ((f | E) | B) by RELAT_1: 71;

      (g | B) = ( - (f | B)) by Th3;

      then

       A18: ( Integral (M,(g | B))) = ( - ( Integral (M,(f | B)))) by A1, A14, A15, A16, A17, Th52, MESFUNC5: 42;

      E = ( dom g) by A1, MESFUNC1:def 7;

      then ( Integral (M,(g | (A \/ B)))) = (( Integral (M,(g | A))) + ( Integral (M,(g | B)))) by A2, A3, A1, MEASUR11: 63, MESFUNC5: 91;

      then ( - ( Integral (M,(f | (A \/ B))))) = ( - (( Integral (M,(f | A))) + ( Integral (M,(f | B))))) by A8, A13, A18, XXREAL_3: 9;

      hence ( Integral (M,(f | (A \/ B)))) = (( Integral (M,(f | A))) + ( Integral (M,(f | B)))) by XXREAL_3: 10;

    end;

    theorem :: MESFUN11:63

    for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, ExtREAL , A,E be Element of S st E = ( dom f) & f is E -measurable & f is nonpositive holds 0 >= ( Integral (M,(f | A)))

    proof

      let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, ExtREAL , A,E be Element of S;

      assume that

       A1: E = ( dom f) and

       A2: f is E -measurable and

       A3: f is nonpositive;

      reconsider E1 = (E /\ A) as Element of S;

      

       A4: ( dom (f | A)) = E1 by A1, RELAT_1: 61;

      

       A5: E1 = (( dom f) /\ E1) by A1, XBOOLE_1: 17, XBOOLE_1: 28;

      f is E1 -measurable by A2, XBOOLE_1: 17, MESFUNC1: 30;

      then

       A6: (f | E1) is E1 -measurable by A5, MESFUNC5: 42;

      (f | E1) = ((f | E) | A) by RELAT_1: 71;

      hence 0 >= ( Integral (M,(f | A))) by A1, A3, A4, A6, Th61, Th1;

    end;

    theorem :: MESFUN11:64

    for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, ExtREAL , A,B,E be Element of S st E = ( dom f) & f is E -measurable & f is nonpositive & A c= B holds ( Integral (M,(f | A))) >= ( Integral (M,(f | B)))

    proof

      let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, ExtREAL , A,B,E be Element of S;

      assume that

       A1: E = ( dom f) and

       A2: f is E -measurable and

       A3: f is nonpositive and

       A4: A c= B;

      set g = ( - f);

      E = ( dom g) by A1, MESFUNC1:def 7;

      then

       A5: ( Integral (M,(g | A))) <= ( Integral (M,(g | B))) by A1, A2, A3, A4, MESFUNC5: 93, MEASUR11: 63;

      reconsider E1 = (E /\ A) as Element of S;

      

       A6: ( dom (f | A)) = E1 by A1, RELAT_1: 61;

      

       A7: E1 = (( dom f) /\ E1) by A1, XBOOLE_1: 17, XBOOLE_1: 28;

      

       A8: f is E1 -measurable by A2, XBOOLE_1: 17, MESFUNC1: 30;

      

       A9: (f | E1) = ((f | E) | A) by RELAT_1: 71;

      (g | A) = ( - (f | A)) by Th3;

      then

       A10: ( Integral (M,(g | A))) = ( - ( Integral (M,(f | A)))) by A1, A6, A7, A8, A9, Th52, MESFUNC5: 42;

      reconsider E2 = (E /\ B) as Element of S;

      

       A11: ( dom (f | B)) = E2 by A1, RELAT_1: 61;

      

       A12: E2 = (( dom f) /\ E2) by A1, XBOOLE_1: 17, XBOOLE_1: 28;

      

       A13: f is E2 -measurable by A2, XBOOLE_1: 17, MESFUNC1: 30;

      

       A14: (f | E2) = ((f | E) | B) by RELAT_1: 71;

      (g | B) = ( - (f | B)) by Th3;

      then ( Integral (M,(g | B))) = ( - ( Integral (M,(f | B)))) by A1, A11, A12, A13, A14, Th52, MESFUNC5: 42;

      hence ( Integral (M,(f | A))) >= ( Integral (M,(f | B))) by A5, A10, XXREAL_3: 38;

    end;

    begin

    theorem :: MESFUN11:65

    for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, E be Element of S, f be PartFunc of X, ExtREAL st E = ( dom f) & f is E -measurable & f is nonpositive & (M . (E /\ ( eq_dom (f, -infty )))) <> 0 holds ( Integral (M,f)) = -infty

    proof

      let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, E be Element of S, f be PartFunc of X, ExtREAL ;

      assume that

       A1: E = ( dom f) and

       A2: f is E -measurable and

       A3: f is nonpositive and

       A4: (M . (E /\ ( eq_dom (f, -infty )))) <> 0 ;

      set g = ( - f);

      

       A5: E = ( dom g) by A1, MESFUNC1:def 7;

      g = (( - 1) (#) f) by MESFUNC2: 9;

      then ( eq_dom (f, -infty )) = ( eq_dom (g,( -infty * ( - 1)))) by Th9;

      then ( eq_dom (f, -infty )) = ( eq_dom (g, +infty )) by XXREAL_3:def 5;

      then ( Integral (M,g)) = +infty by A1, A2, A3, A4, A5, MESFUNC9: 13, MEASUR11: 63;

      then ( - ( Integral (M,f))) = +infty by A1, A2, Th52;

      hence ( Integral (M,f)) = -infty by XXREAL_3: 6;

    end;

    theorem :: MESFUN11:66

    for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, E be Element of S, f,g be PartFunc of X, ExtREAL st E c= ( dom f) & E c= ( dom g) & f is E -measurable & g is E -measurable & f is nonpositive & (for x be Element of X st x in E holds (g . x) <= (f . x)) holds ( Integral (M,(g | E))) <= ( Integral (M,(f | E)))

    proof

      let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, E be Element of S, f,g be PartFunc of X, ExtREAL ;

      assume that

       A1: E c= ( dom f) and

       A2: E c= ( dom g) and

       A3: f is E -measurable & g is E -measurable and

       A4: f is nonpositive and

       A5: for x be Element of X st x in E holds (g . x) <= (f . x);

      set f1 = ( - f), g1 = ( - g);

      

       A6: E c= ( dom f1) & E c= ( dom g1) by A1, A2, MESFUNC1:def 7;

      

       A7: f1 is E -measurable & g1 is E -measurable by A1, A2, A3, MEASUR11: 63;

      

       A11: for x be Element of X st x in E holds (f1 . x) <= (g1 . x)

      proof

        let x be Element of X;

        assume

         A9: x in E;

        then (f1 . x) = ( - (f . x)) & (g1 . x) = ( - (g . x)) by A6, MESFUNC1:def 7;

        hence (f1 . x) <= (g1 . x) by A5, A9, XXREAL_3: 38;

      end;

      

       A12: (( dom f) /\ E) = E & (( dom g) /\ E) = E by A1, A2, XBOOLE_1: 28;

      

       A14: E = ( dom (f | E)) & E = ( dom (g | E)) by A12, RELAT_1: 61;

      (f1 | E) = ( - (f | E)) & (g1 | E) = ( - (g | E)) by Th3;

      then ( Integral (M,(f1 | E))) = ( - ( Integral (M,(f | E)))) & ( Integral (M,(g1 | E))) = ( - ( Integral (M,(g | E)))) by A3, A12, A14, Th52, MESFUNC5: 42;

      hence ( Integral (M,(g | E))) <= ( Integral (M,(f | E))) by A4, A6, A7, A11, XXREAL_3: 38, MESFUNC9: 15;

    end;

    theorem :: MESFUN11:67

    

     Th67: for X be non empty set, F be Functional_Sequence of X, ExtREAL , S be SigmaField of X, E be Element of S, m be Nat st F is with_the_same_dom & E = ( dom (F . 0 )) & (for n be Nat holds (F . n) is E -measurable & (F . n) is without+infty) holds (( Partial_Sums F) . m) is E -measurable

    proof

      let X be non empty set, F be Functional_Sequence of X, ExtREAL , S be SigmaField of X, E be Element of S, m be Nat;

      assume that

       A1: F is with_the_same_dom and

       A2: E = ( dom (F . 0 )) and

       A3: for n be Nat holds (F . n) is E -measurable & (F . n) is without+infty;

      now

        let n be Nat;

        E = ( dom (F . n)) by A1, A2, MESFUNC8:def 2;

        then ( - (F . n)) is E -measurable by A3, MEASUR11: 63;

        hence (( - F) . n) is E -measurable by Th37;

        (F . n) is without+infty by A3;

        then ( - (F . n)) is without-infty;

        hence (( - F) . n) is without-infty by Th37;

      end;

      then (( Partial_Sums ( - F)) . m) is E -measurable by MESFUNC9: 41;

      then (( - ( Partial_Sums F)) . m) is E -measurable by Th42;

      then

       A5: ( - (( Partial_Sums F) . m)) is E -measurable by Th37;

      ( dom (( Partial_Sums F) . m)) = E by A1, A2, A3, Th46, MESFUNC9: 29;

      then ( dom ( - (( Partial_Sums F) . m))) = E by MESFUNC1:def 7;

      then ( - ( - (( Partial_Sums F) . m))) is E -measurable by A5, MEASUR11: 63;

      hence (( Partial_Sums F) . m) is E -measurable by DBLSEQ_3: 2;

    end;

    theorem :: MESFUN11:68

    for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, F be Functional_Sequence of X, ExtREAL , E be Element of S, I be ExtREAL_sequence, m be Nat st E = ( dom (F . 0 )) & F is additive & F is with_the_same_dom & (for n be Nat holds (F . n) is E -measurable & (F . n) is nonpositive & (I . n) = ( Integral (M,(F . n)))) holds ( Integral (M,(( Partial_Sums F) . m))) = (( Partial_Sums I) . m)

    proof

      let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, F be Functional_Sequence of X, ExtREAL , E be Element of S, I be ExtREAL_sequence, m be Nat;

      assume that

       A1: E = ( dom (F . 0 )) and

       A2: F is additive and

       A3: F is with_the_same_dom and

       A4: for n be Nat holds (F . n) is E -measurable & (F . n) is nonpositive & (I . n) = ( Integral (M,(F . n)));

      set G = ( - F), J = ( - I);

      (G . 0 ) = ( - (F . 0 )) by Th37;

      then

       A5: E = ( dom (G . 0 )) by A1, MESFUNC1:def 7;

      

       A6: G is with_the_same_dom by A3, Th40;

      

       A7: E = ( dom (( Partial_Sums F) . m)) by A1, A2, A3, MESFUNC9: 29;

      

       A8: for n be Nat holds (F . n) is E -measurable & (F . n) is without+infty

      proof

        let n be Nat;

        thus (F . n) is E -measurable by A4;

        (F . n) is nonpositive by A4;

        hence (F . n) is without+infty;

      end;

      for n be Nat holds (G . n) is E -measurable & (G . n) is nonnegative & (J . n) = ( Integral (M,(G . n)))

      proof

        let n be Nat;

        

         A9: (F . n) is nonpositive & (I . n) = ( Integral (M,(F . n))) by A4;

        

         A10: (G . n) = ( - (F . n)) by Th37;

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

        then

         A11: n in ( dom J) by ORDINAL1:def 12;

        

         A12: ( dom (F . n)) = E by A1, A3, MESFUNC8:def 2;

        hence (G . n) is E -measurable by A4, A10, MEASUR11: 63;

        thus (G . n) is nonnegative by A9, A10;

        ( Integral (M,(G . n))) = ( - ( Integral (M,(F . n)))) by A4, A10, A12, Th52;

        hence (J . n) = ( Integral (M,(G . n))) by A9, A11, MESFUNC1:def 7;

      end;

      then ( Integral (M,(( Partial_Sums G) . m))) = (( Partial_Sums J) . m) by A5, A2, A6, Th41, MESFUNC9: 46;

      then ( Integral (M,(( - ( Partial_Sums F)) . m))) = (( Partial_Sums J) . m) by Th42;

      then ( Integral (M,(( - ( Partial_Sums F)) . m))) = ( - (( Partial_Sums I) . m)) by Th43;

      then ( Integral (M,( - (( Partial_Sums F) . m)))) = ( - (( Partial_Sums I) . m)) by Th37;

      then ( - ( Integral (M,(( Partial_Sums F) . m)))) = ( - (( Partial_Sums I) . m)) by A1, A3, A7, A8, Th67, Th52;

      hence ( Integral (M,(( Partial_Sums F) . m))) = (( Partial_Sums I) . m) by XXREAL_3: 10;

    end;

    theorem :: MESFUN11:69

    for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, F be Functional_Sequence of X, ExtREAL , E be Element of S, f be PartFunc of X, ExtREAL st E c= ( dom f) & f is nonpositive & f is E -measurable & (for n be Nat holds (F . n) is_simple_func_in S & (F . n) is nonpositive & E c= ( dom (F . n))) & (for x be Element of X st x in E holds (F # x) is summable & (f . x) = ( Sum (F # x))) holds ex I be ExtREAL_sequence st (for n be Nat holds (I . n) = ( Integral (M,((F . n) | E)))) & I is summable & ( Integral (M,(f | E))) = ( Sum I)

    proof

      let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, F be Functional_Sequence of X, ExtREAL , E be Element of S, f be PartFunc of X, ExtREAL ;

      assume that

       A1: E c= ( dom f) and

       A2: f is nonpositive and

       A3: f is E -measurable and

       A4: for n be Nat holds (F . n) is_simple_func_in S & (F . n) is nonpositive & E c= ( dom (F . n)) and

       A5: for x be Element of X st x in E holds (F # x) is summable & (f . x) = ( Sum (F # x));

      set g = ( - f), G = ( - F);

      

       A6: E c= ( dom g) by A1, MESFUNC1:def 7;

      now

        let n be Nat;

        (F . n) is nonpositive by A4;

        then ( - (F . n)) is without-infty;

        hence (G . n) is without-infty by Th37;

      end;

      then

       A7: G is additive by Th47;

      

       A8: for n be Nat holds (G . n) is_simple_func_in S & (G . n) is nonnegative & E c= ( dom (G . n))

      proof

        let n be Nat;

        (( - 1) (#) (F . n)) is_simple_func_in S by A4, MESFUNC5: 39;

        then ( - (F . n)) is_simple_func_in S by MESFUNC2: 9;

        hence (G . n) is_simple_func_in S by Th37;

        (F . n) is nonpositive by A4;

        then ( - (F . n)) is nonnegative;

        hence (G . n) is nonnegative by Th37;

        E c= ( dom (F . n)) by A4;

        then E c= ( dom ( - (F . n))) by MESFUNC1:def 7;

        hence E c= ( dom (G . n)) by Th37;

      end;

      

       A9: for x be Element of X st x in E holds (G # x) is summable & (g . x) = ( Sum (G # x))

      proof

        let x be Element of X;

        assume

         A10: x in E;

        then

         A11: (F # x) is summable & (f . x) = ( Sum (F # x)) by A5;

        hence (G # x) is summable by Th48;

        (g . x) = ( - (f . x)) by A6, A10, MESFUNC1:def 7;

        hence (g . x) = ( Sum (G # x)) by A11, Th48;

      end;

      consider J be ExtREAL_sequence such that

       A12: (for n be Nat holds (J . n) = ( Integral (M,((G . n) | E)))) & J is summable & ( Integral (M,(g | E))) = ( Sum J) by A2, A1, A3, A6, A7, A8, A9, MESFUNC9: 47, MEASUR11: 63;

      take I = ( - J);

      thus for n be Nat holds (I . n) = ( Integral (M,((F . n) | E)))

      proof

        let n be Nat;

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

        then n in ( dom I) by ORDINAL1:def 12;

        then (I . n) = ( - (J . n)) by MESFUNC1:def 7;

        then

         A13: (I . n) = ( - ( Integral (M,((G . n) | E)))) by A12;

        

         A14: E c= ( dom (G . n)) by A8;

        

         A15: (G . n) is E -measurable by A8, MESFUNC2: 34;

        (G . n) = ( - (F . n)) by Th37;

        then (F . n) = ( - (G . n)) by Th36;

        hence (I . n) = ( Integral (M,((F . n) | E))) by A13, A14, A15, Th55;

      end;

      thus I is summable by A12, Th45;

      

       A16: ( Integral (M,(g | E))) = ( - ( Integral (M,(f | E)))) by A1, A3, Th55;

      ( Partial_Sums J) is convergent by A12, MESFUNC9:def 2;

      

      then ( lim ( - ( Partial_Sums J))) = ( - ( lim ( Partial_Sums J))) by DBLSEQ_3: 17

      .= ( - ( Integral (M,(g | E)))) by A12, MESFUNC9:def 3;

      then ( lim ( Partial_Sums I)) = ( - ( Integral (M,(g | E)))) by Th44;

      hence ( Integral (M,(f | E))) = ( Sum I) by A16, MESFUNC9:def 3;

    end;

    theorem :: MESFUN11:70

    for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, E be Element of S, f be PartFunc of X, ExtREAL st E c= ( dom f) & f is nonpositive & f is E -measurable holds ex F be Functional_Sequence of X, ExtREAL st F is additive & (for n be Nat holds (F . n) is_simple_func_in S & (F . n) is nonpositive & (F . n) is E -measurable) & (for x be Element of X st x in E holds (F # x) is summable & (f . x) = ( Sum (F # x))) & ex I be ExtREAL_sequence st (for n be Nat holds (I . n) = ( Integral (M,((F . n) | E)))) & I is summable & ( Integral (M,(f | E))) = ( Sum I)

    proof

      let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, E be Element of S, f be PartFunc of X, ExtREAL ;

      assume that

       A1: E c= ( dom f) and

       A2: f is nonpositive and

       A3: f is E -measurable;

      set g = ( - f);

      

       A4: E c= ( dom g) by A1, MESFUNC1:def 7;

      then

      consider G be Functional_Sequence of X, ExtREAL such that

       A5: G is additive & (for n be Nat holds (G . n) is_simple_func_in S & (G . n) is nonnegative & (G . n) is E -measurable) & (for x be Element of X st x in E holds (G # x) is summable & (g . x) = ( Sum (G # x))) & ex J be ExtREAL_sequence st (for n be Nat holds (J . n) = ( Integral (M,((G . n) | E)))) & J is summable & ( Integral (M,(g | E))) = ( Sum J) by A1, A2, A3, MESFUNC9: 48, MEASUR11: 63;

      take F = ( - G);

      thus F is additive by A5, Th41;

      thus for n be Nat holds (F . n) is_simple_func_in S & (F . n) is nonpositive & (F . n) is E -measurable

      proof

        let n be Nat;

        (( - 1) (#) (G . n)) is_simple_func_in S by A5, MESFUNC5: 39;

        then ( - (G . n)) is_simple_func_in S by MESFUNC2: 9;

        hence

         A6: (F . n) is_simple_func_in S by Th37;

        (G . n) is nonnegative by A5;

        then ( - (G . n)) is nonpositive;

        hence (F . n) is nonpositive by Th37;

        thus (F . n) is E -measurable by A6, MESFUNC2: 34;

      end;

      thus for x be Element of X st x in E holds (F # x) is summable & (f . x) = ( Sum (F # x))

      proof

        let x be Element of X;

        assume

         A7: x in E;

        then

         A8: (G # x) is summable & (g . x) = ( Sum (G # x)) by A5;

        hence (F # x) is summable by Th48;

        (g . x) = ( - (f . x)) by A7, A4, MESFUNC1:def 7;

        then (f . x) = ( - ( Sum (G # x))) by A8;

        hence (f . x) = ( Sum (F # x)) by A8, Th48;

      end;

      thus ex I be ExtREAL_sequence st (for n be Nat holds (I . n) = ( Integral (M,((F . n) | E)))) & I is summable & ( Integral (M,(f | E))) = ( Sum I)

      proof

        consider J be ExtREAL_sequence such that

         A9: (for n be Nat holds (J . n) = ( Integral (M,((G . n) | E)))) & J is summable & ( Integral (M,(g | E))) = ( Sum J) by A5;

        take I = ( - J);

        thus for n be Nat holds (I . n) = ( Integral (M,((F . n) | E)))

        proof

          let n be Nat;

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

          then

           A10: n in ( dom I) by ORDINAL1:def 12;

          

           A11: (J . n) = ( Integral (M,((G . n) | E))) by A9;

          (F . n) = ( - (G . n)) by Th37;

          then

           A12: ((F . n) | E) = ( - ((G . n) | E)) by Th3;

          

           A13: (G . n) is_simple_func_in S by A5;

          then

          consider GG be Finite_Sep_Sequence of S such that

           A14: ( dom (G . n)) = ( union ( rng GG)) & for k be Nat, x,y be Element of X st k in ( dom GG) & x in (GG . k) & y in (GG . k) holds ((G . n) . x) = ((G . n) . y) by MESFUNC2:def 4;

          reconsider V = ( union ( rng GG)) as Element of S by MESFUNC2: 31;

          reconsider VE = (V /\ E) as Element of S;

          

           A15: VE = ( dom ((G . n) | E)) by A14, RELAT_1: 61;

          ((G . n) | E) is VE -measurable by A13, MESFUNC2: 34, MESFUNC5: 34;

          then ( Integral (M,((F . n) | E))) = ( - ( Integral (M,((G . n) | E)))) by A12, A15, Th52;

          hence (I . n) = ( Integral (M,((F . n) | E))) by A10, A11, MESFUNC1:def 7;

        end;

        thus I is summable by A9, Th45;

        

         A16: ( Partial_Sums J) is convergent by A9, MESFUNC9:def 2;

        

         A17: ( Sum I) = ( lim ( Partial_Sums I)) by MESFUNC9:def 3

        .= ( lim ( - ( Partial_Sums J))) by Th44

        .= ( - ( lim ( Partial_Sums J))) by A16, DBLSEQ_3: 17

        .= ( - ( Integral (M,(g | E)))) by A9, MESFUNC9:def 3;

        

         A18: ( dom (f | E)) = E by A1, RELAT_1: 62;

        

         A19: E = (( dom f) /\ E) by A1, XBOOLE_1: 28;

        (g | E) = ( - (f | E)) by Th3;

        then ( Integral (M,(g | E))) = ( - ( Integral (M,(f | E)))) by A3, A18, A19, Th52, MESFUNC5: 42;

        hence ( Integral (M,(f | E))) = ( Sum I) by A17;

      end;

    end;

    theorem :: MESFUN11:71

    for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, F be Functional_Sequence of X, ExtREAL , E be Element of S st E = ( dom (F . 0 )) & F is with_the_same_dom & (for n be Nat holds (F . n) is nonpositive & (F . n) is E -measurable) holds ex FF be sequence of ( Funcs ( NAT ,( PFuncs (X, ExtREAL )))) st for n be Nat holds (for m be Nat holds ((FF . n) . m) is_simple_func_in S & ( dom ((FF . n) . m)) = ( dom (F . n))) & (for m be Nat holds ((FF . n) . m) is nonpositive) & (for j,k be Nat st j <= k holds for x be Element of X st x in ( dom (F . n)) holds (((FF . n) . j) . x) >= (((FF . n) . k) . x)) & for x be Element of X st x in ( dom (F . n)) holds ((FF . n) # x) is convergent & ( lim ((FF . n) # x)) = ((F . n) . x)

    proof

      let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, F be Functional_Sequence of X, ExtREAL , E be Element of S;

      assume that

       A1: E = ( dom (F . 0 )) and

       A2: F is with_the_same_dom and

       A3: for n be Nat holds (F . n) is nonpositive & (F . n) is E -measurable;

      defpred Q[ Element of NAT , set] means for G be Functional_Sequence of X, ExtREAL st $2 = G holds (for m be Nat holds (G . m) is_simple_func_in S & ( dom (G . m)) = ( dom (F . $1))) & (for m be Nat holds (G . m) is nonpositive) & (for j,k be Nat st j <= k holds for x be Element of X st x in ( dom (F . $1)) holds ((G . j) . x) >= ((G . k) . x)) & (for x be Element of X st x in ( dom (F . $1)) holds (G # x) is convergent & ( lim (G # x)) = ((F . $1) . x));

      

       A4: for n be Element of NAT holds ex G be Functional_Sequence of X, ExtREAL st (for m be Nat holds (G . m) is_simple_func_in S & ( dom (G . m)) = ( dom (F . n))) & (for m be Nat holds (G . m) is nonpositive) & (for j,k be Nat st j <= k holds for x be Element of X st x in ( dom (F . n)) holds ((G . j) . x) >= ((G . k) . x)) & for x be Element of X st x in ( dom (F . n)) holds (G # x) is convergent & ( lim (G # x)) = ((F . n) . x)

      proof

        let n be Element of NAT ;

        

         A5: (F . n) is E -measurable by A3;

        (F . n) is nonpositive by A3;

        hence thesis by A1, A2, A5, Th56, MESFUNC8:def 2;

      end;

      

       A7: for n be Element of NAT holds ex G be Element of ( Funcs ( NAT ,( PFuncs (X, ExtREAL )))) st Q[n, G]

      proof

        let n be Element of NAT ;

        consider G be Functional_Sequence of X, ExtREAL such that

         A8: for m be Nat holds (G . m) is_simple_func_in S & ( dom (G . m)) = ( dom (F . n)) and

         A9: for m be Nat holds (G . m) is nonpositive and

         A10: for j,k be Nat st j <= k holds for x be Element of X st x in ( dom (F . n)) holds ((G . j) . x) >= ((G . k) . x) and

         A11: for x be Element of X st x in ( dom (F . n)) holds (G # x) is convergent & ( lim (G # x)) = ((F . n) . x) by A4;

        reconsider G as Element of ( Funcs ( NAT ,( PFuncs (X, ExtREAL )))) by FUNCT_2: 8;

        take G;

        thus thesis by A8, A9, A10, A11;

      end;

      consider FF be sequence of ( Funcs ( NAT ,( PFuncs (X, ExtREAL )))) such that

       A12: for n be Element of NAT holds Q[n, (FF . n)] from FUNCT_2:sch 3( A7);

      take FF;

      thus for n be Nat holds (for m be Nat holds ((FF . n) . m) is_simple_func_in S & ( dom ((FF . n) . m)) = ( dom (F . n))) & (for m be Nat holds ((FF . n) . m) is nonpositive) & (for j,k be Nat st j <= k holds for x be Element of X st x in ( dom (F . n)) holds (((FF . n) . j) . x) >= (((FF . n) . k) . x)) & for x be Element of X st x in ( dom (F . n)) holds ((FF . n) # x) is convergent & ( lim ((FF . n) # x)) = ((F . n) . x)

      proof

        let n be Nat;

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

        for G be Functional_Sequence of X, ExtREAL st (FF . n1) = G holds (for m be Nat holds (G . m) is_simple_func_in S & ( dom (G . m)) = ( dom (F . n1))) & (for m be Nat holds (G . m) is nonpositive) & (for j,k be Nat st j <= k holds for x be Element of X st x in ( dom (F . n1)) holds ((G . j) . x) >= ((G . k) . x)) & for x be Element of X st x in ( dom (F . n1)) holds (G # x) is convergent & ( lim (G # x)) = ((F . n1) . x) by A12;

        hence thesis;

      end;

    end;

    theorem :: MESFUN11:72

    for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, F be Functional_Sequence of X, ExtREAL , E be Element of S st E = ( dom (F . 0 )) & F is additive & F is with_the_same_dom & (for n be Nat holds (F . n) is E -measurable & (F . n) is nonpositive) holds ex I be ExtREAL_sequence st for n be Nat holds (I . n) = ( Integral (M,(F . n))) & ( Integral (M,(( Partial_Sums F) . n))) = (( Partial_Sums I) . n)

    proof

      let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, F be Functional_Sequence of X, ExtREAL , E be Element of S;

      assume that

       A1: E = ( dom (F . 0 )) and

       A2: F is additive and

       A3: F is with_the_same_dom and

       A4: for n be Nat holds (F . n) is E -measurable & (F . n) is nonpositive;

      set G = ( - F);

      (G . 0 ) = ( - (F . 0 )) by Th37;

      then

       A5: E = ( dom (G . 0 )) by A1, MESFUNC1:def 7;

      

       A7: G is with_the_same_dom by A3, Th40;

      for n be Nat holds (G . n) is E -measurable & (G . n) is nonnegative

      proof

        let n be Nat;

        E = ( dom (F . n)) & (F . n) is E -measurable by A4, A1, A3, MESFUNC8:def 2;

        then ( - (F . n)) is E -measurable by MEASUR11: 63;

        hence (G . n) is E -measurable by Th37;

        (F . n) is nonpositive by A4;

        then ( - (F . n)) is nonnegative;

        hence (G . n) is nonnegative by Th37;

      end;

      then

      consider J be ExtREAL_sequence such that

       A8: for n be Nat holds (J . n) = ( Integral (M,(G . n))) & ( Integral (M,(( Partial_Sums G) . n))) = (( Partial_Sums J) . n) by A5, A7, A2, Th41, MESFUNC9: 50;

      set I = ( - J);

      take I;

      

       A10: for n be Nat holds (F . n) is E -measurable & (F . n) is without+infty

      proof

        let n be Nat;

        thus (F . n) is E -measurable by A4;

        (F . n) is nonpositive by A4;

        hence (F . n) is without+infty;

      end;

      hereby

        let n be Nat;

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

        then n in ( dom I) by ORDINAL1:def 12;

        then (I . n) = ( - (J . n)) by MESFUNC1:def 7;

        then

         A9: (I . n) = ( - ( Integral (M,(G . n)))) by A8;

        E = ( dom (F . n)) & (F . n) is E -measurable & (G . n) = ( - (F . n)) by A4, A1, A3, Th37, MESFUNC8:def 2;

        then ( Integral (M,(G . n))) = ( - ( Integral (M,(F . n)))) by Th52;

        hence (I . n) = ( Integral (M,(F . n))) by A9;

        

         A11: E = ( dom (( Partial_Sums F) . n)) by A1, A2, A3, MESFUNC9: 29;

        (( Partial_Sums G) . n) = (( - ( Partial_Sums F)) . n) by Th42

        .= ( - (( Partial_Sums F) . n)) by Th37;

        then

         A13: ( Integral (M,(( Partial_Sums G) . n))) = ( - ( Integral (M,(( Partial_Sums F) . n)))) by A10, A1, A3, A11, Th52, Th67;

        (( Partial_Sums I) . n) = ( - (( Partial_Sums J) . n)) by Th43

        .= ( - ( Integral (M,(( Partial_Sums G) . n)))) by A8;

        hence ( Integral (M,(( Partial_Sums F) . n))) = (( Partial_Sums I) . n) by A13;

      end;

    end;

    theorem :: MESFUN11:73

    for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, F be Functional_Sequence of X, ExtREAL , E be Element of S st E c= ( dom (F . 0 )) & F is additive & F is with_the_same_dom & (for n be Nat holds (F . n) is nonpositive & (F . n) is E -measurable) & (for x be Element of X st x in E holds (F # x) is summable) holds ex I be ExtREAL_sequence st (for n be Nat holds (I . n) = ( Integral (M,((F . n) | E)))) & I is summable & ( Integral (M,(( lim ( Partial_Sums F)) | E))) = ( Sum I)

    proof

      let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, F be Functional_Sequence of X, ExtREAL , E be Element of S;

      assume that

       A1: E c= ( dom (F . 0 )) and

       A2: F is additive and

       A3: F is with_the_same_dom and

       A4: for n be Nat holds (F . n) is nonpositive & (F . n) is E -measurable and

       A5: for x be Element of X st x in E holds (F # x) is summable;

      set G = ( - F);

      (G . 0 ) = ( - (F . 0 )) by Th37;

      then

       A6: E c= ( dom (G . 0 )) by A1, MESFUNC1:def 7;

      

       A7: G is additive by A2, Th41;

      

       A8: G is with_the_same_dom by A3, Th40;

      

       A9: for n be Nat holds (G . n) is nonnegative & (G . n) is E -measurable

      proof

        let n be Nat;

        (F . n) is nonpositive by A4;

        then ( - (F . n)) is nonnegative;

        hence (G . n) is nonnegative by Th37;

        E c= ( dom (F . n)) by A1, A3, MESFUNC8:def 2;

        then ( - (F . n)) is E -measurable by A4, MEASUR11: 63;

        hence (G . n) is E -measurable by Th37;

      end;

      

       A10: for x be Element of X st x in E holds (G # x) is summable

      proof

        let x be Element of X;

        assume x in E;

        then (F # x) is summable by A5;

        hence (G # x) is summable by Th48;

      end;

      then

      consider J be ExtREAL_sequence such that

       A11: (for n be Nat holds (J . n) = ( Integral (M,((G . n) | E)))) & J is summable & ( Integral (M,(( lim ( Partial_Sums G)) | E))) = ( Sum J) by A6, A7, A3, Th40, A9, MESFUNC9: 51;

      take I = ( - J);

      thus for n be Nat holds (I . n) = ( Integral (M,((F . n) | E)))

      proof

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        then

         A14: n in ( dom I) by FUNCT_2:def 1;

        

         A12: E c= ( dom (G . n)) by A6, A3, Th40, MESFUNC8:def 2;

        (G . n) = ( - (F . n)) by Th37;

        then (F . n) = ( - (G . n)) by Th36;

        then ( Integral (M,((F . n) | E))) = ( - ( Integral (M,((G . n) | E)))) by A12, A9, Th55;

        then (J . n) = ( - ( Integral (M,((F . n) | E)))) by A11;

        then (I . n) = ( - ( - ( Integral (M,((F . n) | E))))) by A14, MESFUNC1:def 7;

        hence (I . n) = ( Integral (M,((F . n) | E)));

      end;

      thus I is summable by A11, Th45;

      

       A15: ( Partial_Sums J) is convergent by A11, MESFUNC9:def 2;

      

       A16: ( Sum I) = ( lim ( Partial_Sums I)) by MESFUNC9:def 3

      .= ( lim ( - ( Partial_Sums J))) by Th44

      .= ( - ( lim ( Partial_Sums J))) by A15, DBLSEQ_3: 17

      .= ( - ( Integral (M,(( lim ( Partial_Sums G)) | E)))) by A11, MESFUNC9:def 3;

      deffunc F1( Nat) = ((F . $1) | E);

      consider F1 be Functional_Sequence of X, ExtREAL such that

       A17: for n be Nat holds (F1 . n) = F1(n) from SEQFUNC:sch 1;

      reconsider F1 as additive with_the_same_dom Functional_Sequence of X, ExtREAL by A2, A3, A17, MESFUNC9: 18, MESFUNC9: 31;

      

       A18: ( lim ( Partial_Sums F1)) = (( lim ( Partial_Sums F)) | E) by A1, A2, A3, A17, Th50;

      deffunc G1( Nat) = ((G . $1) | E);

      consider G1 be Functional_Sequence of X, ExtREAL such that

       A19: for n be Nat holds (G1 . n) = G1(n) from SEQFUNC:sch 1;

      reconsider G1 as additive with_the_same_dom Functional_Sequence of X, ExtREAL by A7, A8, A19, MESFUNC9: 18, MESFUNC9: 31;

      

       A20: ( lim ( Partial_Sums G1)) = (( lim ( Partial_Sums G)) | E) by A6, A7, A19, A3, Th40, Th50;

      for n be Element of NAT holds (F1 . n) = (( - G1) . n)

      proof

        let n be Element of NAT ;

        (G . n) = ( - (F . n)) by Th37;

        

        then

         A21: (( - G) . n) = ( - ( - (F . n))) by Th37

        .= (F . n) by DBLSEQ_3: 2;

        

         A22: (F1 . n) = ((F . n) | E) by A17;

        (( - G1) . n) = ( - (G1 . n)) by Th37;

        then (( - G1) . n) = ( - ((G . n) | E)) by A19;

        then (( - G1) . n) = (( - (G . n)) | E) by Th3;

        hence (F1 . n) = (( - G1) . n) by A21, A22, Th37;

      end;

      then

       A23: F1 = ( - G1) by FUNCT_2:def 7;

      (G1 . 0 ) = ((G . 0 ) | E) by A19;

      then

       A24: ( dom (G1 . 0 )) = E by A6, RELAT_1: 62;

      then

       A25: for x be Element of X st x in ( dom (G1 . 0 )) holds (G1 # x) is summable by A6, A10, A19, MESFUNC9: 21;

      then

       A26: ( lim ( Partial_Sums F1)) = ( - ( lim ( Partial_Sums G1))) by A23, Th49;

      for n be Nat holds (G1 . n) is E -measurable & (G1 . n) is without-infty

      proof

        let n be Nat;

        thus (G1 . n) is E -measurable by A6, A9, A19, A3, Th40, MESFUNC9: 20;

        ((G . n) | E) is nonnegative by A9, MESFUNC5: 15;

        hence (G1 . n) is without-infty by A19;

      end;

      then

       A27: for n be Nat holds (( Partial_Sums G1) . n) is E -measurable by MESFUNC9: 41;

      ( dom ( lim ( Partial_Sums G1))) = ( dom (( Partial_Sums G1) . 0 )) by MESFUNC8:def 9

      .= ( dom (G1 . 0 )) by MESFUNC9:def 4;

      then ( Integral (M,(( - ( lim ( Partial_Sums G1))) | E))) = ( - ( Integral (M,(( lim ( Partial_Sums G1)) | E)))) by A24, A25, A27, Th55, MESFUNC9: 44;

      hence ( Integral (M,(( lim ( Partial_Sums F)) | E))) = ( Sum I) by A16, A18, A20, A26;

    end;

    theorem :: MESFUN11:74

    for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, F be Functional_Sequence of X, ExtREAL , E be Element of S st E = ( dom (F . 0 )) & (F . 0 ) is nonpositive & F is with_the_same_dom & (for n be Nat holds (F . n) is E -measurable) & (for n,m be Nat st n <= m holds for x be Element of X st x in E holds ((F . n) . x) >= ((F . m) . x)) & (for x be Element of X st x in E holds (F # x) is convergent) holds ex I be ExtREAL_sequence st (for n be Nat holds (I . n) = ( Integral (M,(F . n)))) & I is convergent & ( Integral (M,( lim F))) = ( lim I)

    proof

      let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, F be Functional_Sequence of X, ExtREAL , E be Element of S;

      assume that

       A1: E = ( dom (F . 0 )) and

       A2: (F . 0 ) is nonpositive and

       A3: F is with_the_same_dom and

       A4: for n be Nat holds (F . n) is E -measurable and

       A5: for n,m be Nat st n <= m holds for x be Element of X st x in E holds ((F . n) . x) >= ((F . m) . x) and

       A6: for x be Element of X st x in E holds (F # x) is convergent;

      set G = ( - F);

      

       A7: (G . 0 ) = ( - (F . 0 )) by Th37;

      then

       A8: E = ( dom (G . 0 )) by A1, MESFUNC1:def 7;

      

       A11: for n be Nat holds (G . n) is E -measurable

      proof

        let n be Nat;

        E = ( dom (F . n)) by A1, A3, MESFUNC8:def 2;

        then ( - (F . n)) is E -measurable by A4, MEASUR11: 63;

        hence (G . n) is E -measurable by Th37;

      end;

      

       A13: for n,m be Nat st n <= m holds for x be Element of X st x in E holds ((G . n) . x) <= ((G . m) . x)

      proof

        let n,m be Nat;

        assume

         A14: n <= m;

        let x be Element of X;

        assume

         A15: x in E;

        then

         A17: x in ( dom (G . n)) & x in ( dom (G . m)) by A8, A3, Th40, MESFUNC8:def 2;

        (G . n) = ( - (F . n)) & (G . m) = ( - (F . m)) by Th37;

        then ((G . n) . x) = ( - ((F . n) . x)) & ((G . m) . x) = ( - ((F . m) . x)) by A17, MESFUNC1:def 7;

        hence ((G . n) . x) <= ((G . m) . x) by A15, A5, A14, XXREAL_3: 38;

      end;

      

       A18: for x be Element of X st x in E holds (G # x) is convergent

      proof

        let x be Element of X;

        assume x in E;

        then (F # x) is convergent by A6;

        then ( - (F # x)) is convergent by DBLSEQ_3: 17;

        hence (G # x) is convergent by Th38;

      end;

      consider J be ExtREAL_sequence such that

       A19: (for n be Nat holds (J . n) = ( Integral (M,(G . n)))) & J is convergent & ( Integral (M,( lim G))) = ( lim J) by A8, A2, A7, A3, Th40, A11, A13, A18, MESFUNC9: 52;

      set I = ( - J);

      take I;

      thus for n be Nat holds (I . n) = ( Integral (M,(F . n)))

      proof

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        then

         A20: n in ( dom I) by FUNCT_2:def 1;

        

         A21: ( dom (F . n)) = E by A1, A3, MESFUNC8:def 2;

        (G . n) = ( - (F . n)) by Th37;

        then ( Integral (M,(G . n))) = ( - ( Integral (M,(F . n)))) by A21, A4, Th52;

        then (J . n) = ( - ( Integral (M,(F . n)))) by A19;

        then (I . n) = ( - ( - ( Integral (M,(F . n))))) by A20, MESFUNC1:def 7;

        hence (I . n) = ( Integral (M,(F . n)));

      end;

      thus I is convergent by A19, DBLSEQ_3: 17;

      

       A23: ( lim I) = ( - ( Integral (M,( lim G)))) by A19, DBLSEQ_3: 17;

      

       A24: E = ( dom ( lim F)) by A1, MESFUNC8:def 9;

      then

       A25: ( dom ( - ( lim F))) = E by MESFUNC1:def 7;

      then

       A26: ( dom ( lim G)) = ( dom ( - ( lim F))) by A8, MESFUNC8:def 9;

      for x be Element of X st x in ( dom ( lim G)) holds (( lim G) . x) = (( - ( lim F)) . x)

      proof

        let x be Element of X;

        assume

         A27: x in ( dom ( lim G));

        then

         A30: (( lim G) . x) = ( lim (G # x)) by MESFUNC8:def 9;

        

         A28: (F # x) is convergent by A27, A26, A25, A6;

        (G # x) = ( - (F # x)) by Th38;

        then

         A29: ( lim (G # x)) = ( - ( lim (F # x))) by A28, DBLSEQ_3: 17;

        ( lim (F # x)) = (( lim F) . x) by A27, A26, A25, A24, MESFUNC8:def 9;

        hence (( lim G) . x) = (( - ( lim F)) . x) by A29, A30, A27, A26, MESFUNC1:def 7;

      end;

      then ( lim G) = ( - ( lim F)) by A26, PARTFUN1: 5;

      then ( Integral (M,( lim G))) = ( - ( Integral (M,( lim F)))) by A1, A3, A4, A6, A24, Th52, MESFUNC8: 25;

      hence ( Integral (M,( lim F))) = ( lim I) by A23;

    end;