mesfun10.miz



    begin

    reserve X for non empty set,

F for with_the_same_dom Functional_Sequence of X, ExtREAL ,

seq,seq1,seq2 for ExtREAL_sequence,

x for Element of X,

a,r for R_eal,

n,m,k for Nat;

    theorem :: MESFUN10:1

    

     Th1: (for n be Nat holds (seq1 . n) <= (seq2 . n)) implies ( inf ( rng seq1)) <= ( inf ( rng seq2))

    proof

      assume

       A1: for n be Nat holds (seq1 . n) <= (seq2 . n);

      now

        let x be ExtReal;

         A2:

        now

          let n be Element of NAT ;

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

          then

           A3: (seq1 . n) in ( rng seq1) by FUNCT_1:def 3;

          

           A4: (seq1 . n) <= (seq2 . n) by A1;

          ( inf ( rng seq1)) is LowerBound of ( rng seq1) by XXREAL_2:def 4;

          then ( inf ( rng seq1)) <= (seq1 . n) by A3, XXREAL_2:def 2;

          hence ( inf ( rng seq1)) <= (seq2 . n) by A4, XXREAL_0: 2;

        end;

        assume x in ( rng seq2);

        then ex z be object st z in ( dom seq2) & x = (seq2 . z) by FUNCT_1:def 3;

        hence ( inf ( rng seq1)) <= x by A2;

      end;

      then ( inf ( rng seq1)) is LowerBound of ( rng seq2) by XXREAL_2:def 2;

      hence thesis by XXREAL_2:def 4;

    end;

    theorem :: MESFUN10:2

    

     Th2: (for n be Nat holds (seq1 . n) <= (seq2 . n)) implies (( inferior_realsequence seq1) . k) <= (( inferior_realsequence seq2) . k) & (( superior_realsequence seq1) . k) <= (( superior_realsequence seq2) . k)

    proof

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

      assume

       A1: for n be Nat holds (seq1 . n) <= (seq2 . n);

       A2:

      now

        let n be Nat;

        

         A3: ((seq2 ^\ k1) . n) = (seq2 . (n + k)) by NAT_1:def 3;

        ((seq1 ^\ k1) . n) = (seq1 . (n + k)) by NAT_1:def 3;

        hence ((seq1 ^\ k1) . n) <= ((seq2 ^\ k1) . n) by A1, A3;

      end;

      then ( sup (seq1 ^\ k1)) <= ( sup (seq2 ^\ k1)) by MESFUNC5: 55;

      then

       A4: (( superior_realsequence seq1) . k) <= ( sup (seq2 ^\ k1)) by RINFSUP2: 27;

      ( inf (seq1 ^\ k1)) <= ( inf (seq2 ^\ k1)) by A2, Th1;

      then (( inferior_realsequence seq1) . k) <= ( inf (seq2 ^\ k1)) by RINFSUP2: 27;

      hence thesis by A4, RINFSUP2: 27;

    end;

    theorem :: MESFUN10:3

    

     Th3: (for n be Nat holds (seq1 . n) <= (seq2 . n)) implies ( lim_inf seq1) <= ( lim_inf seq2) & ( lim_sup seq1) <= ( lim_sup seq2)

    proof

      assume for n be Nat holds (seq1 . n) <= (seq2 . n);

      then for n be Nat holds (( inferior_realsequence seq1) . n) <= (( inferior_realsequence seq2) . n) & (( superior_realsequence seq1) . n) <= (( superior_realsequence seq2) . n) by Th2;

      hence thesis by Th1, MESFUNC5: 55;

    end;

    theorem :: MESFUN10:4

    

     Th4: (for n be Nat holds (seq . n) >= a) implies ( inf seq) >= a

    proof

      assume

       A1: for n be Nat holds (seq . n) >= a;

      now

        let x be ExtReal;

        assume x in ( rng seq);

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

        hence x >= a by A1;

      end;

      then a is LowerBound of ( rng seq) by XXREAL_2:def 2;

      hence thesis by XXREAL_2:def 4;

    end;

    theorem :: MESFUN10:5

    

     Th5: (for n be Nat holds (seq . n) <= a) implies ( sup seq) <= a

    proof

      assume

       A1: for n be Nat holds (seq . n) <= a;

      now

        let x be ExtReal;

        assume x in ( rng seq);

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

        hence x <= a by A1;

      end;

      then a is UpperBound of ( rng seq) by XXREAL_2:def 1;

      hence thesis by XXREAL_2:def 3;

    end;

    theorem :: MESFUN10:6

    

     Th6: for n be Element of NAT st x in ( dom ( inf (F ^\ n))) holds (( inf (F ^\ n)) . x) = ( inf ((F # x) ^\ n))

    proof

      let n be Element of NAT ;

      now

        reconsider g = F as sequence of ( PFuncs (X, ExtREAL ));

        let k be Element of NAT ;

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

        then (((F ^\ n) # x) . k) = ((g . (n + k)) . x) by NAT_1:def 3;

        then (((F ^\ n) # x) . k) = ((F # x) . (n + k)) by MESFUNC5:def 13;

        hence (((F ^\ n) # x) . k) = (((F # x) ^\ n) . k) by NAT_1:def 3;

      end;

      then

       A1: ((F ^\ n) # x) = ((F # x) ^\ n) by FUNCT_2: 63;

      assume x in ( dom ( inf (F ^\ n)));

      hence thesis by A1, MESFUNC8:def 3;

    end;

    reserve S for SigmaField of X,

M for sigma_Measure of S,

E for Element of S;

    ::$Notion-Name

    theorem :: MESFUN10:7

    

     Th7: E = ( dom (F . 0 )) & (for n holds (F . n) is nonnegative & (F . n) is E -measurable) implies ex I be ExtREAL_sequence st (for n holds (I . n) = ( Integral (M,(F . n)))) & ( Integral (M,( lim_inf F))) <= ( lim_inf I)

    proof

      assume that

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

       A2: for n holds (F . n) is nonnegative & (F . n) is E -measurable;

      set H = ( inferior_realsequence F);

      deffunc G( Element of NAT ) = ( inf (F ^\ $1));

      consider G be Function such that

       A3: ( dom G) = NAT & for n be Element of NAT holds (G . n) = G(n) from FUNCT_1:sch 4;

      now

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        then (G . n) = ( inf (F ^\ n)) by A3;

        hence (G . n) is PartFunc of X, ExtREAL ;

      end;

      then

      reconsider G as Functional_Sequence of X, ExtREAL by A3, SEQFUNC: 1;

      

       A4: for n be Element of NAT holds (G . n) = (( inferior_realsequence F) . n)

      proof

        let n be Element of NAT ;

        (( inferior_realsequence F) . n) = ( inf (F ^\ n)) by MESFUNC8: 8;

        hence thesis by A3;

      end;

      then

       A5: G = ( inferior_realsequence F) by FUNCT_2: 63;

      reconsider G as with_the_same_dom Functional_Sequence of X, ExtREAL by A4, FUNCT_2: 63;

      

       A6: ( dom (H . 0 )) = ( dom (G . 0 )) by A4;

      

       A7: for n,m be Nat, x be Element of X st n <= m & x in E holds ((G . n) . x) <= ((G . m) . x) & ((G # x) . n) <= ((G # x) . m)

      proof

        let n,m be Nat, x be Element of X;

        reconsider n1 = n, m1 = m as Element of NAT by ORDINAL1:def 12;

        assume that

         A8: n <= m and

         A9: x in E;

        (H # x) = ( inferior_realsequence (F # x)) by A1, A9, MESFUNC8: 7;

        then ((H # x) . n1) <= ((H # x) . m1) by A8, RINFSUP2: 7;

        then ((H . n) . x) <= ((H # x) . m) by MESFUNC5:def 13;

        hence ((G . n) . x) <= ((G . m) . x) by A5, MESFUNC5:def 13;

        then ((G # x) . n) <= ((G . m) . x) by MESFUNC5:def 13;

        hence thesis by MESFUNC5:def 13;

      end;

       A10:

      now

        let x be Element of X;

        assume x in E;

        then for n,m be Nat st m <= n holds ((G # x) . m) <= ((G # x) . n) by A7;

        then (G # x) is non-decreasing by RINFSUP2: 7;

        hence (G # x) is convergent by RINFSUP2: 37;

      end;

      deffunc I( Element of NAT ) = ( Integral (M,(F . $1)));

      consider I be sequence of ExtREAL such that

       A11: for n be Element of NAT holds (I . n) = I(n) from FUNCT_2:sch 4;

      

       A12: for n be Nat holds (G . n) is E -measurable by A1, A2, A5, MESFUNC8: 20;

      

       A13: ( dom (H . 0 )) = ( dom (F . 0 )) by MESFUNC8:def 5;

      then

       A14: ( dom ( lim G)) = E by A1, A6, MESFUNC8:def 9;

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

      proof

        let x be object;

        assume

         A15: x in ( dom (G . 0 ));

        then

        reconsider x as Element of X;

         A16:

        now

          let n be Nat;

          (F . n) is nonnegative by A2;

          then 0 <= ((F . n) . x) by SUPINF_2: 51;

          then 0 <= ((F # x) . ( 0 + n)) by MESFUNC5:def 13;

          hence 0. <= (((F # x) ^\ 0 ) . n) by NAT_1:def 3;

        end;

        ((F ^\ 0 ) . 0 ) = (F . ( 0 + 0 )) by NAT_1:def 3;

        then ( dom ( inf (F ^\ 0 ))) = ( dom (F . 0 )) by MESFUNC8:def 3;

        then (( inf (F ^\ 0 )) . x) = ( inf ((F # x) ^\ 0 )) by A13, A6, A15, Th6;

        then ((G . 0 ) . x) = ( inf ((F # x) ^\ 0 )) by A3;

        hence thesis by A16, Th4;

      end;

      then

       A17: (G . 0 ) is nonnegative by SUPINF_2: 52;

      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) by A7;

      then

      consider J be ExtREAL_sequence such that

       A18: for n be Nat holds (J . n) = ( Integral (M,(G . n))) and

       A19: J is convergent and

       A20: ( Integral (M,( lim G))) = ( lim J) by A1, A13, A6, A17, A12, A10, MESFUNC9: 52;

      reconsider I as ExtREAL_sequence;

      for n be Nat holds (J . n) <= (I . n)

      proof

        let n be Nat;

        

         A21: ( dom (F . n)) = E by A1, MESFUNC8:def 2;

        

         A22: (F . n) is nonnegative by A2;

        

         A23: n is Element of NAT by ORDINAL1:def 12;

         A24:

        now

          let x be Element of X;

          assume

           A25: x in ( dom (G . n));

          (( inferior_realsequence (F # x)) . n) <= ((F # x) . n) by RINFSUP2: 8;

          then ((H . n) . x) <= ((F # x) . n) by A5, A25, MESFUNC8:def 5;

          then ((H . n) . x) <= ((F . n) . x) by MESFUNC5:def 13;

          hence ((G . n) . x) <= ((F . n) . x) by A4, A23;

        end;

        

         A26: (F . n) is E -measurable by A2;

        

         A27: (G . n) is E -measurable by A1, A2, A5, MESFUNC8: 20;

        

         A28: ( dom (G . n)) = E by A1, A13, A6, MESFUNC8:def 2;

         A29:

        now

          let x be object;

          assume

           A30: x in ( dom (G . n));

           0 <= ((G . 0 ) . x) by A17, SUPINF_2: 51;

          hence 0 <= ((G . n) . x) by A7, A28, A30;

        end;

        then (G . n) is nonnegative by SUPINF_2: 52;

        then ( integral+ (M,(G . n))) <= ( integral+ (M,(F . n))) by A21, A28, A26, A27, A22, A24, MESFUNC5: 85;

        then ( Integral (M,(G . n))) <= ( integral+ (M,(F . n))) by A28, A27, A29, MESFUNC5: 88, SUPINF_2: 52;

        then

         A31: ( Integral (M,(G . n))) <= ( Integral (M,(F . n))) by A21, A26, A22, MESFUNC5: 88;

        (I . n) = ( Integral (M,(F . n))) by A11, A23;

        hence thesis by A18, A31;

      end;

      then ( lim_inf J) <= ( lim_inf I) by Th3;

      then

       A32: ( lim J) <= ( lim_inf I) by A19, RINFSUP2: 41;

      

       A33: ( dom ( sup G)) = E by A1, A13, A6, MESFUNC8:def 4;

      now

        let x be Element of X;

        assume

         A34: x in ( dom ( lim G));

        then for n,m be Nat st m <= n holds ((G # x) . m) <= ((G # x) . n) by A7, A14;

        then (G # x) is non-decreasing by RINFSUP2: 7;

        then

         A35: ( lim (G # x)) = ( sup (G # x)) by RINFSUP2: 37;

        (( sup G) . x) = ( sup (G # x)) by A14, A33, A34, MESFUNC8:def 4;

        hence (( lim G) . x) = (( sup G) . x) by A34, A35, MESFUNC8:def 9;

      end;

      then

       A36: ( lim G) = ( sup G) by A14, A33, PARTFUN1: 5;

      take I;

      for n be Nat holds (I . n) = ( Integral (M,(F . n)))

      proof

        let n be Nat;

        n is Element of NAT by ORDINAL1:def 12;

        hence thesis by A11;

      end;

      hence thesis by A5, A20, A36, A32, MESFUNC8: 11;

    end;

    begin

    theorem :: MESFUN10:8

    

     Th8: for Y be non empty Subset of ExtREAL , r be R_eal st r in REAL holds ( sup ( {r} + Y)) = (( sup {r}) + ( sup Y))

    proof

      let Y be non empty Subset of ExtREAL ;

      let r be R_eal;

      set X = {r};

      assume

       A1: r in REAL ;

      set W = (X + Y);

      

       A2: ( - r) <> -infty by A1, XXREAL_3: 23;

      

       A3: ( - r) <> +infty by A1, XXREAL_3: 23;

      now

        let z be object;

        assume z in (( - X) + W);

        then

        consider x,y be R_eal such that

         A4: z = (x + y) and

         A5: x in ( - X) and

         A6: y in W;

        consider x1,y1 be R_eal such that

         A7: y = (x1 + y1) and

         A8: x1 in X and

         A9: y1 in Y by A6;

        ( - x) in ( - ( - X)) by A5;

        then ( - x) in X;

        then ( - x) = r by TARSKI:def 1;

        then z = (( - r) + (r + y1)) by A4, A8, A7, TARSKI:def 1;

        then z = ((( - r) + r) + y1) by A1, A3, A2, XXREAL_3: 29;

        then z = ( 0. + y1) by XXREAL_3: 7;

        hence z in Y by A9, XXREAL_3: 4;

      end;

      then

       A10: (( - X) + W) c= Y by TARSKI:def 3;

      

       A11: r in X by TARSKI:def 1;

      now

        let z be object;

        assume

         A12: z in Y;

        then

        reconsider y = z as Element of ExtREAL ;

        ((r + y) - r) = ((( - r) + r) + y) by A1, A3, A2, XXREAL_3: 29;

        then ((r + y) - r) = ( 0. + y) by XXREAL_3: 7;

        then

         A13: y = ((r + y) - r) by XXREAL_3: 4;

        

         A14: ( - r) in ( - X) by A11;

        (r + y) in W by A11, A12;

        hence z in (( - X) + W) by A14, A13;

      end;

      then Y c= (( - X) + W) by TARSKI:def 3;

      then Y = (( - X) + W) by A10, XBOOLE_0:def 10;

      then ( sup Y) <= (( sup W) + ( sup ( - X))) by SUPINF_2: 8;

      then ( sup Y) <= (( sup (X + Y)) + ( - ( inf X))) by SUPINF_2: 15;

      then ( sup Y) <= (( sup (X + Y)) - r) by XXREAL_2: 13;

      then (r + ( sup Y)) <= ( sup (X + Y)) by A1, XXREAL_3: 57;

      then

       A15: (( sup X) + ( sup Y)) <= ( sup (X + Y)) by XXREAL_2: 11;

      ( sup (X + Y)) <= (( sup X) + ( sup Y)) by SUPINF_2: 8;

      hence thesis by A15, XXREAL_0: 1;

    end;

    theorem :: MESFUN10:9

    

     Th9: for Y be non empty Subset of ExtREAL , r be R_eal st r in REAL holds ( inf ( {r} + Y)) = (( inf {r}) + ( inf Y))

    proof

      let Y be non empty Subset of ExtREAL ;

      let r be R_eal;

      set X = {r};

      assume

       A1: r in REAL ;

      set W = (X + Y);

      set Z = ( - X);

      

       A2: ( - r) <> -infty by A1, XXREAL_3: 23;

      

       A3: ( - r) <> +infty by A1, XXREAL_3: 23;

      now

        let z be object;

        assume z in (Z + W);

        then

        consider x,y be R_eal such that

         A4: z = (x + y) and

         A5: x in Z and

         A6: y in W;

        consider x1,y1 be R_eal such that

         A7: y = (x1 + y1) and

         A8: x1 in X and

         A9: y1 in Y by A6;

        ( - x) in ( - Z) by A5;

        then ( - x) in X;

        then ( - x) = r by TARSKI:def 1;

        then z = (( - r) + (r + y1)) by A4, A8, A7, TARSKI:def 1;

        then z = ((( - r) + r) + y1) by A1, A3, A2, XXREAL_3: 29;

        then z = ( 0. + y1) by XXREAL_3: 7;

        hence z in Y by A9, XXREAL_3: 4;

      end;

      then

       A10: (Z + W) c= Y by TARSKI:def 3;

      

       A11: r in X by TARSKI:def 1;

      now

        let z be object;

        assume

         A12: z in Y;

        then

        reconsider y = z as Element of ExtREAL ;

        ((r + y) - r) = ((( - r) + r) + y) by A1, A3, A2, XXREAL_3: 29;

        then ((r + y) - r) = ( 0. + y) by XXREAL_3: 7;

        then

         A13: y = ((r + y) - r) by XXREAL_3: 4;

        

         A14: ( - r) in Z by A11;

        (r + y) in W by A11, A12;

        hence z in (Z + W) by A14, A13;

      end;

      then Y c= (Z + W) by TARSKI:def 3;

      then Y = (Z + W) by A10, XBOOLE_0:def 10;

      then ( inf Y) >= (( inf W) + ( inf Z)) by SUPINF_2: 9;

      then ( inf Y) >= (( inf (X + Y)) + ( - ( sup X))) by SUPINF_2: 14;

      then ( inf Y) >= (( inf (X + Y)) - r) by XXREAL_2: 11;

      then (r + ( inf Y)) >= ( inf (X + Y)) by A1, XXREAL_3: 52;

      then

       A15: (( inf X) + ( inf Y)) >= ( inf (X + Y)) by XXREAL_2: 13;

      ( inf (X + Y)) >= (( inf X) + ( inf Y)) by SUPINF_2: 9;

      hence thesis by A15, XXREAL_0: 1;

    end;

    theorem :: MESFUN10:10

    

     Th10: r in REAL & (for n be Nat holds (seq1 . n) = (r + (seq2 . n))) implies ( lim_inf seq1) = (r + ( lim_inf seq2)) & ( lim_sup seq1) = (r + ( lim_sup seq2))

    proof

      assume that

       A1: r in REAL and

       A2: for n be Nat holds (seq1 . n) = (r + (seq2 . n));

      reconsider R1 = ( rng ( inferior_realsequence seq1)), R2 = ( rng ( inferior_realsequence seq2)), P1 = ( rng ( superior_realsequence seq1)), P2 = ( rng ( superior_realsequence seq2)) as non empty Subset of ExtREAL ;

      now

        let z be object;

        assume z in ( {r} + R2);

        then

        consider z2,z3 be R_eal such that

         A3: z = (z2 + z3) and

         A4: z2 in {r} and

         A5: z3 in R2;

        consider n be object such that

         A6: n in NAT and

         A7: (( inferior_realsequence seq2) . n) = z3 by A5, FUNCT_2: 11;

        reconsider n as Element of NAT by A6;

        consider Y2 be non empty Subset of ExtREAL such that

         A8: Y2 = { (seq2 . k) where k be Nat : n <= k } and

         A9: z3 = ( inf Y2) by A7, RINFSUP2:def 6;

        consider Y1 be non empty Subset of ExtREAL such that

         A10: Y1 = { (seq1 . k) where k be Nat : n <= k } and

         A11: (( inferior_realsequence seq1) . n) = ( inf Y1) by RINFSUP2:def 6;

        now

          let w be object;

          

           A12: r in {r} by TARSKI:def 1;

          assume w in Y1;

          then

          consider k1 be Nat such that

           A13: w = (seq1 . k1) and

           A14: n <= k1 by A10;

          reconsider w1 = w as R_eal by A13;

          

           A15: (seq2 . k1) in Y2 by A8, A14;

          w1 = (r + (seq2 . k1)) by A2, A13;

          hence w in ( {r} + Y2) by A12, A15;

        end;

        then

         A16: Y1 c= ( {r} + Y2) by TARSKI:def 3;

        now

          let w be object;

          assume w in ( {r} + Y2);

          then

          consider w1,w2 be R_eal such that

           A17: w = (w1 + w2) and

           A18: w1 in {r} and

           A19: w2 in Y2;

          consider k2 be Nat such that

           A20: w2 = (seq2 . k2) and

           A21: n <= k2 by A8, A19;

          w1 = r by A18, TARSKI:def 1;

          then w = (seq1 . k2) by A2, A17, A20;

          hence w in Y1 by A10, A21;

        end;

        then ( {r} + Y2) c= Y1 by TARSKI:def 3;

        then Y1 = ( {r} + Y2) by A16, XBOOLE_0:def 10;

        then ( inf Y1) = (( inf {r}) + ( inf Y2)) by A1, Th9;

        then ( inf Y1) = (r + ( inf Y2)) by XXREAL_2: 13;

        then z = (( inferior_realsequence seq1) . n) by A4, A3, A9, A11, TARSKI:def 1;

        hence z in R1 by FUNCT_2: 4;

      end;

      then

       A22: ( {r} + R2) c= R1 by TARSKI:def 3;

      now

        let z be object;

        assume z in ( {r} + P2);

        then

        consider z2,z3 be R_eal such that

         A23: z = (z2 + z3) and

         A24: z2 in {r} and

         A25: z3 in P2;

        consider n be object such that

         A26: n in NAT and

         A27: (( superior_realsequence seq2) . n) = z3 by A25, FUNCT_2: 11;

        reconsider n as Element of NAT by A26;

        consider Y2 be non empty Subset of ExtREAL such that

         A28: Y2 = { (seq2 . k) where k be Nat : n <= k } and

         A29: z3 = ( sup Y2) by A27, RINFSUP2:def 7;

        consider Y1 be non empty Subset of ExtREAL such that

         A30: Y1 = { (seq1 . k) where k be Nat : n <= k } and

         A31: (( superior_realsequence seq1) . n) = ( sup Y1) by RINFSUP2:def 7;

        now

          let w be object;

          

           A32: r in {r} by TARSKI:def 1;

          assume w in Y1;

          then

          consider k1 be Nat such that

           A33: w = (seq1 . k1) and

           A34: n <= k1 by A30;

          reconsider w1 = w as R_eal by A33;

          

           A35: (seq2 . k1) in Y2 by A28, A34;

          w1 = (r + (seq2 . k1)) by A2, A33;

          hence w in ( {r} + Y2) by A32, A35;

        end;

        then

         A36: Y1 c= ( {r} + Y2) by TARSKI:def 3;

        now

          let w be object;

          assume w in ( {r} + Y2);

          then

          consider w1,w2 be R_eal such that

           A37: w = (w1 + w2) and

           A38: w1 in {r} and

           A39: w2 in Y2;

          consider k2 be Nat such that

           A40: w2 = (seq2 . k2) and

           A41: n <= k2 by A28, A39;

          w1 = r by A38, TARSKI:def 1;

          then w = (seq1 . k2) by A2, A37, A40;

          hence w in Y1 by A30, A41;

        end;

        then ( {r} + Y2) c= Y1 by TARSKI:def 3;

        then Y1 = ( {r} + Y2) by A36, XBOOLE_0:def 10;

        then ( sup Y1) = (( sup {r}) + ( sup Y2)) by A1, Th8;

        then ( sup Y1) = (r + ( sup Y2)) by XXREAL_2: 11;

        then z = (( superior_realsequence seq1) . n) by A24, A23, A29, A31, TARSKI:def 1;

        hence z in P1 by FUNCT_2: 4;

      end;

      then

       A42: ( {r} + P2) c= P1 by TARSKI:def 3;

      now

        let z be object;

        assume z in R1;

        then

        consider n be object such that

         A43: n in NAT and

         A44: (( inferior_realsequence seq1) . n) = z by FUNCT_2: 11;

        reconsider n as Element of NAT by A43;

        consider Y1 be non empty Subset of ExtREAL such that

         A45: Y1 = { (seq1 . k) where k be Nat : n <= k } and

         A46: z = ( inf Y1) by A44, RINFSUP2:def 6;

        consider Y2 be non empty Subset of ExtREAL such that

         A47: Y2 = { (seq2 . k) where k be Nat : n <= k } and

         A48: (( inferior_realsequence seq2) . n) = ( inf Y2) by RINFSUP2:def 6;

        now

          let w be object;

          

           A49: r in {r} by TARSKI:def 1;

          assume w in Y1;

          then

          consider k1 be Nat such that

           A50: w = (seq1 . k1) and

           A51: n <= k1 by A45;

          reconsider w1 = w as R_eal by A50;

          

           A52: (seq2 . k1) in Y2 by A47, A51;

          w1 = (r + (seq2 . k1)) by A2, A50;

          hence w in ( {r} + Y2) by A49, A52;

        end;

        then

         A53: Y1 c= ( {r} + Y2) by TARSKI:def 3;

        now

          let w be object;

          assume w in ( {r} + Y2);

          then

          consider w1,w2 be R_eal such that

           A54: w = (w1 + w2) and

           A55: w1 in {r} and

           A56: w2 in Y2;

          consider k2 be Nat such that

           A57: w2 = (seq2 . k2) and

           A58: n <= k2 by A47, A56;

          w1 = r by A55, TARSKI:def 1;

          then w = (seq1 . k2) by A2, A54, A57;

          hence w in Y1 by A45, A58;

        end;

        then ( {r} + Y2) c= Y1 by TARSKI:def 3;

        then Y1 = ( {r} + Y2) by A53, XBOOLE_0:def 10;

        then ( inf Y1) = (( inf {r}) + ( inf Y2)) by A1, Th9;

        then

         A59: ( inf Y1) = (r + ( inf Y2)) by XXREAL_2: 13;

        

         A60: (( inferior_realsequence seq2) . n) in R2 by FUNCT_2: 4;

        r in {r} by TARSKI:def 1;

        hence z in ( {r} + R2) by A46, A48, A59, A60;

      end;

      then R1 c= ( {r} + R2) by TARSKI:def 3;

      then R1 = ( {r} + R2) by A22, XBOOLE_0:def 10;

      then ( sup R1) = (( sup {r}) + ( sup R2)) by A1, Th8;

      hence ( lim_inf seq1) = (r + ( lim_inf seq2)) by XXREAL_2: 11;

      now

        let z be object;

        assume z in P1;

        then

        consider n be object such that

         A61: n in NAT and

         A62: (( superior_realsequence seq1) . n) = z by FUNCT_2: 11;

        reconsider n as Element of NAT by A61;

        consider Y1 be non empty Subset of ExtREAL such that

         A63: Y1 = { (seq1 . k) where k be Nat : n <= k } and

         A64: z = ( sup Y1) by A62, RINFSUP2:def 7;

        consider Y2 be non empty Subset of ExtREAL such that

         A65: Y2 = { (seq2 . k) where k be Nat : n <= k } and

         A66: (( superior_realsequence seq2) . n) = ( sup Y2) by RINFSUP2:def 7;

        now

          let w be object;

          

           A67: r in {r} by TARSKI:def 1;

          assume w in Y1;

          then

          consider k1 be Nat such that

           A68: w = (seq1 . k1) and

           A69: n <= k1 by A63;

          reconsider w1 = w as R_eal by A68;

          

           A70: (seq2 . k1) in Y2 by A65, A69;

          w1 = (r + (seq2 . k1)) by A2, A68;

          hence w in ( {r} + Y2) by A67, A70;

        end;

        then

         A71: Y1 c= ( {r} + Y2) by TARSKI:def 3;

        now

          let w be object;

          assume w in ( {r} + Y2);

          then

          consider w1,w2 be R_eal such that

           A72: w = (w1 + w2) and

           A73: w1 in {r} and

           A74: w2 in Y2;

          consider k2 be Nat such that

           A75: w2 = (seq2 . k2) and

           A76: n <= k2 by A65, A74;

          w1 = r by A73, TARSKI:def 1;

          then w = (seq1 . k2) by A2, A72, A75;

          hence w in Y1 by A63, A76;

        end;

        then ( {r} + Y2) c= Y1 by TARSKI:def 3;

        then Y1 = ( {r} + Y2) by A71, XBOOLE_0:def 10;

        then ( sup Y1) = (( sup {r}) + ( sup Y2)) by A1, Th8;

        then

         A77: ( sup Y1) = (r + ( sup Y2)) by XXREAL_2: 11;

        

         A78: (( superior_realsequence seq2) . n) in P2 by FUNCT_2: 4;

        r in {r} by TARSKI:def 1;

        hence z in ( {r} + P2) by A64, A66, A77, A78;

      end;

      then P1 c= ( {r} + P2) by TARSKI:def 3;

      then P1 = ( {r} + P2) by A42, XBOOLE_0:def 10;

      then ( inf P1) = (( inf {r}) + ( inf P2)) by A1, Th9;

      hence thesis by XXREAL_2: 13;

    end;

    reserve F1,F2 for Functional_Sequence of X, ExtREAL ,

f,g,P for PartFunc of X, ExtREAL ;

    theorem :: MESFUN10:11

    

     Th11: ( dom (F1 . 0 )) = ( dom (F2 . 0 )) & F1 is with_the_same_dom & (f " { +infty }) = {} & (f " { -infty }) = {} & (for n be Nat holds (F1 . n) = (f + (F2 . n))) implies ( lim_inf F1) = (f + ( lim_inf F2)) & ( lim_sup F1) = (f + ( lim_sup F2))

    proof

      assume that

       A1: ( dom (F1 . 0 )) = ( dom (F2 . 0 )) and

       A2: F1 is with_the_same_dom and

       A3: (f " { +infty }) = {} and

       A4: (f " { -infty }) = {} and

       A5: for n be Nat holds (F1 . n) = (f + (F2 . n));

      

       A6: (F1 . 0 ) = (f + (F2 . 0 )) by A5;

      

       A7: ( dom (f + (F2 . 0 ))) = ((( dom f) /\ ( dom (F2 . 0 ))) \ (((f " { -infty }) /\ ((F2 . 0 ) " { +infty })) \/ ((f " { +infty }) /\ ((F2 . 0 ) " { -infty })))) by MESFUNC1:def 3;

      

       A8: ( dom (f + ( lim_sup F2))) = ((( dom f) /\ ( dom ( lim_sup F2))) \ (((f " { -infty }) /\ (( lim_sup F2) " { +infty })) \/ ((f " { +infty }) /\ (( lim_sup F2) " { -infty })))) by MESFUNC1:def 3;

      then

       A9: ( dom (f + ( lim_sup F2))) = (( dom f) /\ ( dom (F2 . 0 ))) by A3, A4, MESFUNC8:def 8;

      then

       A10: ( dom ( lim_sup F1)) = ( dom (f + ( lim_sup F2))) by A3, A4, A6, A7, MESFUNC8:def 8;

      

       A11: ( dom (f + ( lim_inf F2))) = ((( dom f) /\ ( dom ( lim_inf F2))) \ (((f " { -infty }) /\ (( lim_inf F2) " { +infty })) \/ ((f " { +infty }) /\ (( lim_inf F2) " { -infty })))) by MESFUNC1:def 3;

      then

       A12: ( dom (f + ( lim_inf F2))) = (( dom f) /\ ( dom (F2 . 0 ))) by A3, A4, MESFUNC8:def 7;

      then

       A13: ( dom ( lim_inf F1)) = ( dom (f + ( lim_inf F2))) by A3, A4, A6, A7, MESFUNC8:def 7;

      

       A14: ( dom ( lim_inf F2)) = ( dom (F2 . 0 )) by MESFUNC8:def 7;

      

       A15: ( dom ( lim_inf F1)) = ( dom (F1 . 0 )) by MESFUNC8:def 7;

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

      proof

        let x be Element of X;

        assume

         A16: x in ( dom ( lim_inf F1));

        then

         A17: (( lim_inf F1) . x) = ( lim_inf (F1 # x)) by MESFUNC8:def 7;

        

         A18: for n be Nat holds ((F1 # x) . n) = ((f . x) + ((F2 # x) . n))

        proof

          let n be Nat;

          (F1 . n) = (f + (F2 . n)) by A5;

          then ( dom (f + (F2 . n))) = ( dom (F1 . 0 )) by A2, MESFUNC8:def 2;

          then

           A19: x in ( dom (f + (F2 . n))) by A16, MESFUNC8:def 7;

          ((F1 . n) . x) = ((f + (F2 . n)) . x) by A5;

          then ((F1 . n) . x) = ((f . x) + ((F2 . n) . x)) by A19, MESFUNC1:def 3;

          then ((F1 # x) . n) = ((f . x) + ((F2 . n) . x)) by MESFUNC5:def 13;

          hence thesis by MESFUNC5:def 13;

        end;

        

         A20: ( dom (f + ( lim_inf F2))) c= ( dom f) by A3, A4, A11, XBOOLE_1: 17;

        then not (f . x) in { -infty } by A4, A13, A16, FUNCT_1:def 7;

        then

         A21: (f . x) <> -infty by TARSKI:def 1;

         not (f . x) in { +infty } by A3, A13, A16, A20, FUNCT_1:def 7;

        then (f . x) <> +infty by TARSKI:def 1;

        then

         A22: (f . x) in REAL by A21, XXREAL_0: 14;

        x in ( dom (f + ( lim_inf F2))) by A3, A4, A6, A7, A12, A16, MESFUNC8:def 7;

        then

         A23: ((f + ( lim_inf F2)) . x) = ((f . x) + (( lim_inf F2) . x)) by MESFUNC1:def 3;

        (( lim_inf F2) . x) = ( lim_inf (F2 # x)) by A1, A15, A14, A16, MESFUNC8:def 7;

        hence thesis by A22, A18, A17, A23, Th10;

      end;

      hence ( lim_inf F1) = (f + ( lim_inf F2)) by A13, PARTFUN1: 5;

      

       A24: ( dom ( lim_sup F1)) = ( dom (F1 . 0 )) by MESFUNC8:def 8;

      

       A25: ( dom ( lim_sup F2)) = ( dom (F2 . 0 )) by MESFUNC8:def 8;

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

      proof

        let x be Element of X;

        assume

         A26: x in ( dom ( lim_sup F1));

        then

         A27: (( lim_sup F1) . x) = ( lim_sup (F1 # x)) by MESFUNC8:def 8;

        

         A28: for n be Nat holds ((F1 # x) . n) = ((f . x) + ((F2 # x) . n))

        proof

          let n be Nat;

          (F1 . n) = (f + (F2 . n)) by A5;

          then

           A29: ( dom (f + (F2 . n))) = ( dom (F1 . 0 )) by A2, MESFUNC8:def 2;

          ((F1 . n) . x) = ((f + (F2 . n)) . x) by A5;

          then ((F1 . n) . x) = ((f . x) + ((F2 . n) . x)) by A24, A26, A29, MESFUNC1:def 3;

          then ((F1 # x) . n) = ((f . x) + ((F2 . n) . x)) by MESFUNC5:def 13;

          hence thesis by MESFUNC5:def 13;

        end;

        

         A30: ( dom (f + ( lim_sup F2))) c= ( dom f) by A3, A4, A8, XBOOLE_1: 17;

        then not (f . x) in { -infty } by A4, A10, A26, FUNCT_1:def 7;

        then

         A31: (f . x) <> -infty by TARSKI:def 1;

         not (f . x) in { +infty } by A3, A10, A26, A30, FUNCT_1:def 7;

        then (f . x) <> +infty by TARSKI:def 1;

        then

         A32: (f . x) in REAL by A31, XXREAL_0: 14;

        x in ( dom (f + ( lim_sup F2))) by A3, A4, A6, A7, A9, A26, MESFUNC8:def 8;

        then

         A33: ((f + ( lim_sup F2)) . x) = ((f . x) + (( lim_sup F2) . x)) by MESFUNC1:def 3;

        (( lim_sup F2) . x) = ( lim_sup (F2 # x)) by A1, A24, A25, A26, MESFUNC8:def 8;

        hence thesis by A32, A28, A27, A33, Th10;

      end;

      hence thesis by A10, PARTFUN1: 5;

    end;

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

    theorem :: MESFUN10:12

    

     Th12: f is_integrable_on M & g is_integrable_on M implies (f - g) is_integrable_on M

    proof

      assume that

       A1: f is_integrable_on M and

       A2: g is_integrable_on M;

      (( - jj) (#) g) is_integrable_on M by A2, MESFUNC5: 110;

      then ( - g) is_integrable_on M by MESFUNC2: 9;

      then (f + ( - g)) is_integrable_on M by A1, MESFUNC5: 108;

      hence thesis by MESFUNC2: 8;

    end;

    theorem :: MESFUN10:13

    

     Th13: f is_integrable_on M & g is_integrable_on M implies ex E be Element of S st E = (( dom f) /\ ( dom g)) & ( Integral (M,(f - g))) = (( Integral (M,(f | E))) + ( Integral (M,(( - g) | E))))

    proof

      assume that

       A1: f is_integrable_on M and

       A2: g is_integrable_on M;

      (( - jj) (#) g) is_integrable_on M by A2, MESFUNC5: 110;

      then ( - g) is_integrable_on M by MESFUNC2: 9;

      then

      consider E be Element of S such that

       A3: E = (( dom f) /\ ( dom ( - g))) and

       A4: ( Integral (M,(f + ( - g)))) = (( Integral (M,(f | E))) + ( Integral (M,(( - g) | E)))) by A1, MESFUNC5: 109;

      

       A5: ( dom g) = ( dom ( - g)) by MESFUNC1:def 7;

      ( Integral (M,(f - g))) = (( Integral (M,(f | E))) + ( Integral (M,(( - g) | E)))) by A4, MESFUNC2: 8;

      hence thesis by A3, A5;

    end;

    theorem :: MESFUN10:14

    

     Th14: (for n be Nat holds (seq1 . n) = ( - (seq2 . n))) implies ( lim_inf seq2) = ( - ( lim_sup seq1)) & ( lim_sup seq2) = ( - ( lim_inf seq1))

    proof

      assume

       A1: for n be Nat holds (seq1 . n) = ( - (seq2 . n));

      now

        let z be object;

        assume z in ( rng ( inferior_realsequence seq2));

        then

        consider n be object such that

         A2: n in ( dom ( inferior_realsequence seq2)) and

         A3: z = (( inferior_realsequence seq2) . n) by FUNCT_1:def 3;

        reconsider n as Element of NAT by A2;

        consider R2 be non empty Subset of ExtREAL such that

         A4: R2 = { (seq2 . k) where k be Nat : n <= k } and

         A5: z = ( inf R2) by A3, RINFSUP2:def 6;

        reconsider z2 = z as Element of ExtREAL by A3, XXREAL_0:def 1;

        set R1 = { (seq1 . k) where k be Nat : n <= k };

        reconsider R1 as non empty Subset of ExtREAL by RINFSUP2: 5;

        set z1 = ( - z2);

        

         A6: ex K1 be non empty Subset of ExtREAL st K1 = { (seq1 . k) where k be Nat : n <= k } & (( superior_realsequence seq1) . n) = ( sup K1) by RINFSUP2:def 7;

        now

          let x be object;

          assume x in R1;

          then

          consider k be Nat such that

           A7: x = (seq1 . k) and

           A8: n <= k;

          reconsider x1 = x as Element of ExtREAL by A7;

          ( - x1) = ( - ( - (seq2 . k))) by A1, A7;

          then ( - x1) in { (seq2 . k2) where k2 be Nat : n <= k2 } by A8;

          then ( - ( - x1)) in ( - R2) by A4;

          hence x in ( - R2);

        end;

        then

         A9: R1 c= ( - R2) by TARSKI:def 3;

        now

          let x be object;

          assume x in ( - R2);

          then

          consider y be R_eal such that

           A10: x = ( - y) and

           A11: y in R2;

          consider k be Nat such that

           A12: y = (seq2 . k) and

           A13: n <= k by A4, A11;

          (seq1 . k) = ( - (seq2 . k)) by A1;

          hence x in R1 by A10, A12, A13;

        end;

        then ( - R2) c= R1 by TARSKI:def 3;

        then ( - R2) = R1 by A9, XBOOLE_0:def 10;

        then (( superior_realsequence seq1) . n) = z1 by A5, A6, SUPINF_2: 15;

        then

         A14: z1 in ( rng ( superior_realsequence seq1)) by FUNCT_2: 4;

        z2 = ( - z1);

        hence z in ( - ( rng ( superior_realsequence seq1))) by A14;

      end;

      then

       A15: ( rng ( inferior_realsequence seq2)) c= ( - ( rng ( superior_realsequence seq1))) by TARSKI:def 3;

      now

        let z be object;

        assume z in ( rng ( superior_realsequence seq2));

        then

        consider n be object such that

         A16: n in ( dom ( superior_realsequence seq2)) and

         A17: z = (( superior_realsequence seq2) . n) by FUNCT_1:def 3;

        reconsider n as Element of NAT by A16;

        consider R2 be non empty Subset of ExtREAL such that

         A18: R2 = { (seq2 . k) where k be Nat : n <= k } and

         A19: z = ( sup R2) by A17, RINFSUP2:def 7;

        reconsider z2 = z as Element of ExtREAL by A17, XXREAL_0:def 1;

        set R1 = { (seq1 . k) where k be Nat : n <= k };

        reconsider R1 as non empty Subset of ExtREAL by RINFSUP2: 5;

        set z1 = ( - z2);

        

         A20: ex K1 be non empty Subset of ExtREAL st K1 = { (seq1 . k) where k be Nat : n <= k } & (( inferior_realsequence seq1) . n) = ( inf K1) by RINFSUP2:def 6;

        now

          let x be object;

          assume x in R1;

          then

          consider k be Nat such that

           A21: x = (seq1 . k) and

           A22: n <= k;

          reconsider x1 = x as Element of ExtREAL by A21;

          ( - x1) = ( - ( - (seq2 . k))) by A1, A21;

          then ( - x1) in { (seq2 . k2) where k2 be Nat : n <= k2 } by A22;

          then ( - ( - x1)) in ( - R2) by A18;

          hence x in ( - R2);

        end;

        then

         A23: R1 c= ( - R2) by TARSKI:def 3;

        now

          let x be object;

          assume x in ( - R2);

          then

          consider y be R_eal such that

           A24: x = ( - y) and

           A25: y in R2;

          consider k be Nat such that

           A26: y = (seq2 . k) and

           A27: n <= k by A18, A25;

          (seq1 . k) = ( - (seq2 . k)) by A1;

          hence x in R1 by A24, A26, A27;

        end;

        then ( - R2) c= R1 by TARSKI:def 3;

        then ( - R2) = R1 by A23, XBOOLE_0:def 10;

        then (( inferior_realsequence seq1) . n) = z1 by A19, A20, SUPINF_2: 14;

        then

         A28: z1 in ( rng ( inferior_realsequence seq1)) by FUNCT_2: 4;

        z2 = ( - z1);

        hence z in ( - ( rng ( inferior_realsequence seq1))) by A28;

      end;

      then

       A29: ( rng ( superior_realsequence seq2)) c= ( - ( rng ( inferior_realsequence seq1))) by TARSKI:def 3;

      now

        let z be object;

        assume z in ( - ( rng ( superior_realsequence seq1)));

        then

        consider t be R_eal such that

         A30: z = ( - t) and

         A31: t in ( rng ( superior_realsequence seq1));

        consider n be object such that

         A32: n in ( dom ( superior_realsequence seq1)) and

         A33: t = (( superior_realsequence seq1) . n) by A31, FUNCT_1:def 3;

        reconsider n as Element of NAT by A32;

        consider R1 be non empty Subset of ExtREAL such that

         A34: R1 = { (seq1 . k) where k be Nat : n <= k } and

         A35: t = ( sup R1) by A33, RINFSUP2:def 7;

        reconsider z1 = z as Element of ExtREAL by A30;

        set R2 = { (seq2 . k) where k be Nat : n <= k };

        reconsider R2 as non empty Subset of ExtREAL by RINFSUP2: 5;

        

         A36: ex K2 be non empty Subset of ExtREAL st K2 = { (seq2 . k) where k be Nat : n <= k } & (( inferior_realsequence seq2) . n) = ( inf K2) by RINFSUP2:def 6;

        now

          let x be object;

          assume x in R2;

          then

          consider k be Nat such that

           A37: x = (seq2 . k) and

           A38: n <= k;

          reconsider x1 = x as Element of ExtREAL by A37;

          ( - x1) = ( - ( - (seq1 . k))) by A1, A37;

          then ( - x1) in { (seq1 . k2) where k2 be Nat : n <= k2 } by A38;

          then ( - ( - x1)) in ( - R1) by A34;

          hence x in ( - R1);

        end;

        then

         A39: R2 c= ( - R1) by TARSKI:def 3;

        now

          let x be object;

          assume x in ( - R1);

          then

          consider y be R_eal such that

           A40: x = ( - y) and

           A41: y in R1;

          consider k be Nat such that

           A42: y = (seq1 . k) and

           A43: n <= k by A34, A41;

          (seq1 . k) = ( - (seq2 . k)) by A1;

          hence x in R2 by A40, A42, A43;

        end;

        then ( - R1) c= R2 by TARSKI:def 3;

        then ( - R1) = R2 by A39, XBOOLE_0:def 10;

        then (( inferior_realsequence seq2) . n) = z1 by A30, A35, A36, SUPINF_2: 14;

        hence z in ( rng ( inferior_realsequence seq2)) by FUNCT_2: 4;

      end;

      then ( - ( rng ( superior_realsequence seq1))) c= ( rng ( inferior_realsequence seq2)) by TARSKI:def 3;

      then ( rng ( inferior_realsequence seq2)) = ( - ( rng ( superior_realsequence seq1))) by A15, XBOOLE_0:def 10;

      hence ( lim_inf seq2) = ( - ( lim_sup seq1)) by SUPINF_2: 15;

      now

        let z be object;

        assume z in ( - ( rng ( inferior_realsequence seq1)));

        then

        consider t be R_eal such that

         A44: z = ( - t) and

         A45: t in ( rng ( inferior_realsequence seq1));

        consider n be object such that

         A46: n in ( dom ( inferior_realsequence seq1)) and

         A47: t = (( inferior_realsequence seq1) . n) by A45, FUNCT_1:def 3;

        reconsider n as Element of NAT by A46;

        consider R1 be non empty Subset of ExtREAL such that

         A48: R1 = { (seq1 . k) where k be Nat : n <= k } and

         A49: t = ( inf R1) by A47, RINFSUP2:def 6;

        reconsider z1 = z as Element of ExtREAL by A44;

        set R2 = { (seq2 . k) where k be Nat : n <= k };

        reconsider R2 as non empty Subset of ExtREAL by RINFSUP2: 5;

        

         A50: ex K2 be non empty Subset of ExtREAL st K2 = { (seq2 . k) where k be Nat : n <= k } & (( superior_realsequence seq2) . n) = ( sup K2) by RINFSUP2:def 7;

        now

          let x be object;

          assume x in R2;

          then

          consider k be Nat such that

           A51: x = (seq2 . k) and

           A52: n <= k;

          reconsider x1 = x as Element of ExtREAL by A51;

          (seq1 . k) = ( - (seq2 . k)) by A1;

          then ( - x1) in R1 by A48, A51, A52;

          then ( - ( - x1)) in ( - R1);

          hence x in ( - R1);

        end;

        then

         A53: R2 c= ( - R1) by TARSKI:def 3;

        now

          let x be object;

          assume x in ( - R1);

          then

          consider y be R_eal such that

           A54: x = ( - y) and

           A55: y in R1;

          consider k be Nat such that

           A56: y = (seq1 . k) and

           A57: n <= k by A48, A55;

          (seq1 . k) = ( - (seq2 . k)) by A1;

          hence x in R2 by A54, A56, A57;

        end;

        then ( - R1) c= R2 by TARSKI:def 3;

        then ( - R1) = R2 by A53, XBOOLE_0:def 10;

        then (( superior_realsequence seq2) . n) = z1 by A44, A49, A50, SUPINF_2: 15;

        hence z in ( rng ( superior_realsequence seq2)) by FUNCT_2: 4;

      end;

      then ( - ( rng ( inferior_realsequence seq1))) c= ( rng ( superior_realsequence seq2)) by TARSKI:def 3;

      then ( rng ( superior_realsequence seq2)) = ( - ( rng ( inferior_realsequence seq1))) by A29, XBOOLE_0:def 10;

      hence thesis by SUPINF_2: 14;

    end;

    theorem :: MESFUN10:15

    

     Th15: ( dom (F1 . 0 )) = ( dom (F2 . 0 )) & F1 is with_the_same_dom & (for n be Nat holds (F1 . n) = ( - (F2 . n))) implies ( lim_inf F1) = ( - ( lim_sup F2)) & ( lim_sup F1) = ( - ( lim_inf F2))

    proof

      assume that

       A1: ( dom (F1 . 0 )) = ( dom (F2 . 0 )) and

       A2: F1 is with_the_same_dom and

       A3: for n be Nat holds (F1 . n) = ( - (F2 . n));

      

       A4: ( dom ( lim_inf F1)) = ( dom (F1 . 0 )) by MESFUNC8:def 7;

      

       A5: ( dom ( lim_sup F2)) = ( dom (F2 . 0 )) by MESFUNC8:def 8;

       A6:

      now

        let x be Element of X;

        assume

         A7: x in ( dom (F1 . 0 ));

        let n be Nat;

        ( dom (F1 . n)) = ( dom (F1 . 0 )) by A2, MESFUNC8:def 2;

        then

         A8: x in ( dom ( - (F2 . n))) by A3, A7;

        ((F1 . n) . x) = (( - (F2 . n)) . x) by A3;

        then ((F1 . n) . x) = ( - ((F2 . n) . x)) by A8, MESFUNC1:def 7;

        then ((F1 # x) . n) = ( - ((F2 . n) . x)) by MESFUNC5:def 13;

        hence ((F2 # x) . n) = ( - ((F1 # x) . n)) by MESFUNC5:def 13;

      end;

       A9:

      now

        let x be Element of X;

        assume

         A10: x in ( dom ( lim_inf F1));

        then

         A11: (( lim_inf F1) . x) = ( lim_inf (F1 # x)) by MESFUNC8:def 7;

        x in ( dom ( - ( lim_sup F2))) by A1, A4, A5, A10, MESFUNC1:def 7;

        then

         A12: (( - ( lim_sup F2)) . x) = ( - (( lim_sup F2) . x)) by MESFUNC1:def 7;

        

         A13: for n be Nat holds ((F2 # x) . n) = ( - ((F1 # x) . n)) by A4, A6, A10;

        (( lim_sup F2) . x) = ( lim_sup (F2 # x)) by A1, A4, A5, A10, MESFUNC8:def 8;

        hence (( lim_inf F1) . x) = (( - ( lim_sup F2)) . x) by A13, A11, A12, Th14;

      end;

      ( dom ( - ( lim_sup F2))) = ( dom ( lim_sup F2)) by MESFUNC1:def 7;

      hence ( lim_inf F1) = ( - ( lim_sup F2)) by A1, A4, A5, A9, PARTFUN1: 5;

      

       A14: ( dom ( lim_sup F1)) = ( dom (F1 . 0 )) by MESFUNC8:def 8;

      

       A15: ( dom ( lim_inf F2)) = ( dom (F2 . 0 )) by MESFUNC8:def 7;

      

       A16: for x be Element of X st x in ( dom ( lim_sup F1)) holds (( lim_sup F1) . x) = (( - ( lim_inf F2)) . x)

      proof

        let x be Element of X;

        assume

         A17: x in ( dom ( lim_sup F1));

        then

         A18: (( lim_sup F1) . x) = ( lim_sup (F1 # x)) by MESFUNC8:def 8;

        x in ( dom ( - ( lim_inf F2))) by A1, A14, A15, A17, MESFUNC1:def 7;

        then

         A19: (( - ( lim_inf F2)) . x) = ( - (( lim_inf F2) . x)) by MESFUNC1:def 7;

        

         A20: for n be Nat holds ((F2 # x) . n) = ( - ((F1 # x) . n)) by A14, A6, A17;

        (( lim_inf F2) . x) = ( lim_inf (F2 # x)) by A1, A14, A15, A17, MESFUNC8:def 7;

        hence thesis by A20, A18, A19, Th14;

      end;

      ( dom ( - ( lim_inf F2))) = ( dom ( lim_inf F2)) by MESFUNC1:def 7;

      hence thesis by A1, A14, A15, A16, PARTFUN1: 5;

    end;

    theorem :: MESFUN10:16

    

     Th16: E = ( dom (F . 0 )) & E = ( dom P) & (for n be Nat holds (F . n) is E -measurable) & P is_integrable_on M & (for x be Element of X, n be Nat st x in E holds ( |.(F . n).| . x) <= (P . x)) implies (for n be Nat holds |.(F . n).| is_integrable_on M) & |.( lim_inf F).| is_integrable_on M & |.( lim_sup F).| is_integrable_on M

    proof

      assume that

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

       A2: E = ( dom P) and

       A3: for n be Nat holds (F . n) is E -measurable and

       A4: P is_integrable_on M and

       A5: for x be Element of X, n be Nat st x in E holds ( |.(F . n).| . x) <= (P . x);

      

       A6: ( lim_inf F) is E -measurable by A1, A3, MESFUNC8: 24;

      hereby

        let n be Nat;

        

         A7: (F . n) is E -measurable by A3;

        

         A8: E = ( dom (F . n)) by A1, MESFUNC8:def 2;

        now

          let x be Element of X;

          assume

           A9: x in ( dom (F . n));

          then

           A10: x in ( dom |.(F . n).|) by MESFUNC1:def 10;

          ( |.(F . n).| . x) <= (P . x) by A5, A8, A9;

          hence |.((F . n) . x).| <= (P . x) by A10, MESFUNC1:def 10;

        end;

        then (F . n) is_integrable_on M by A2, A4, A8, A7, MESFUNC5: 102;

        hence |.(F . n).| is_integrable_on M by MESFUNC5: 100;

      end;

      

       A11: E = ( dom ( lim_inf F)) by A1, MESFUNC8:def 7;

      

       A12: ( lim_sup F) is E -measurable by A1, A3, MESFUNC8: 23;

      

       A13: for x be Element of X, k be Nat st x in E holds ( - (P . x)) <= ((F # x) . k) & ((F # x) . k) <= (P . x)

      proof

        let x be Element of X, k be Nat;

        assume

         A14: x in E;

        then x in ( dom (F . k)) by A1, MESFUNC8:def 2;

        then

         A15: x in ( dom |.(F . k).|) by MESFUNC1:def 10;

        ( |.(F . k).| . x) <= (P . x) by A5, A14;

        then

         A16: |.((F . k) . x).| <= (P . x) by A15, MESFUNC1:def 10;

        then

         A17: ((F . k) . x) <= (P . x) by EXTREAL1: 23;

        ( - (P . x)) <= ((F . k) . x) by A16, EXTREAL1: 23;

        hence thesis by A17, MESFUNC5:def 13;

      end;

      now

        let x be Element of X;

        assume

         A18: x in ( dom ( lim_inf F));

        then

         A19: x in E by A1, MESFUNC8:def 7;

        for k be Nat holds (( inferior_realsequence (F # x)) . k) <= (P . x)

        proof

          let k be Nat;

          reconsider k1 = k as Nat;

          

           A20: (( inferior_realsequence (F # x)) . k1) <= ((F # x) . k1) by RINFSUP2: 8;

          ((F # x) . k) <= (P . x) by A13, A19;

          hence thesis by A20, XXREAL_0: 2;

        end;

        then ( lim_inf (F # x)) <= (P . x) by Th5;

        then

         A21: (( lim_inf F) . x) <= (P . x) by A18, MESFUNC8:def 7;

        now

          let y be ExtReal;

          assume y in ( rng (F # x));

          then ex k be object st k in ( dom (F # x)) & y = ((F # x) . k) by FUNCT_1:def 3;

          hence ( - (P . x)) <= y by A13, A19;

        end;

        then ( - (P . x)) is LowerBound of ( rng (F # x)) by XXREAL_2:def 2;

        then ( - (P . x)) <= ( inf (F # x)) by XXREAL_2:def 4;

        then ( - (P . x)) <= ( inf ((F # x) ^\ 0 )) by NAT_1: 47;

        then

         A22: ( - (P . x)) <= (( inferior_realsequence (F # x)) . 0 ) by RINFSUP2: 27;

        (( inferior_realsequence (F # x)) . 0 ) <= ( sup ( inferior_realsequence (F # x))) by RINFSUP2: 23;

        then ( - (P . x)) <= ( lim_inf (F # x)) by A22, XXREAL_0: 2;

        then ( - (P . x)) <= (( lim_inf F) . x) by A18, MESFUNC8:def 7;

        hence |.(( lim_inf F) . x).| <= (P . x) by A21, EXTREAL1: 23;

      end;

      then ( lim_inf F) is_integrable_on M by A2, A4, A11, A6, MESFUNC5: 102;

      hence |.( lim_inf F).| is_integrable_on M by MESFUNC5: 100;

      

       A23: E = ( dom ( lim_sup F)) by A1, MESFUNC8:def 8;

      now

        let x be Element of X;

        assume

         A24: x in ( dom ( lim_sup F));

        for k be Nat holds (( superior_realsequence (F # x)) . k) >= ( - (P . x))

        proof

          let k be Nat;

          reconsider k1 = k as Nat;

          

           A25: (( superior_realsequence (F # x)) . k1) >= ((F # x) . k1) by RINFSUP2: 8;

          ((F # x) . k) >= ( - (P . x)) by A23, A13, A24;

          hence thesis by A25, XXREAL_0: 2;

        end;

        then ( lim_sup (F # x)) >= ( - (P . x)) by Th4;

        then

         A26: (( lim_sup F) . x) >= ( - (P . x)) by A24, MESFUNC8:def 8;

        now

          let y be ExtReal;

          assume y in ( rng (F # x));

          then ex k be object st k in ( dom (F # x)) & y = ((F # x) . k) by FUNCT_1:def 3;

          hence (P . x) >= y by A23, A13, A24;

        end;

        then (P . x) is UpperBound of ( rng (F # x)) by XXREAL_2:def 1;

        then (P . x) >= ( sup ( rng (F # x))) by XXREAL_2:def 3;

        then (P . x) >= ( sup ((F # x) ^\ 0 )) by NAT_1: 47;

        then

         A27: (P . x) >= (( superior_realsequence (F # x)) . 0 ) by RINFSUP2: 27;

        (( superior_realsequence (F # x)) . 0 ) >= ( inf ( superior_realsequence (F # x))) by RINFSUP2: 23;

        then (P . x) >= ( lim_sup (F # x)) by A27, XXREAL_0: 2;

        then (P . x) >= (( lim_sup F) . x) by A24, MESFUNC8:def 8;

        hence |.(( lim_sup F) . x).| <= (P . x) by A26, EXTREAL1: 23;

      end;

      then ( lim_sup F) is_integrable_on M by A2, A4, A23, A12, MESFUNC5: 102;

      hence thesis by MESFUNC5: 100;

    end;

    

     Lm1: E = ( dom (F . 0 )) & E = ( dom P) & (for n be Nat holds (F . n) is E -measurable) & P is_integrable_on M & P is nonnegative & (for x be Element of X, n be Nat st x in E holds ( |.(F . n).| . x) <= (P . x)) & ( eq_dom (P, +infty )) = {} implies ex I be ExtREAL_sequence st (for n be Nat holds (I . n) = ( Integral (M,(F . n)))) & ( lim_inf I) >= ( Integral (M,( lim_inf F))) & ( lim_sup I) <= ( Integral (M,( lim_sup F))) & ((for x be Element of X st x in E holds (F # x) is convergent) implies I is convergent & ( lim I) = ( Integral (M,( lim F))))

    proof

      assume that

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

       A2: E = ( dom P) and

       A3: for n be Nat holds (F . n) is E -measurable and

       A4: P is_integrable_on M and

       A5: P is nonnegative and

       A6: for x be Element of X, n be Nat st x in E holds ( |.(F . n).| . x) <= (P . x) and

       A7: ( eq_dom (P, +infty )) = {} ;

      

       A8: E = ( dom ( lim_inf F)) by A1, MESFUNC8:def 7;

      then

       A9: (( lim_inf F) | E) = ( lim_inf F) by RELAT_1: 68;

      deffunc G( Nat) = (P + (F . $1));

      consider G be Function such that

       A10: ( dom G) = NAT & for n be Element of NAT holds (G . n) = G(n) from FUNCT_1:sch 4;

      

       A11: for x be Element of X, k be Nat st x in E holds ( - (P . x)) <= ((F # x) . k) & ((F # x) . k) <= (P . x)

      proof

        let x be Element of X, k be Nat;

        assume

         A12: x in E;

        then x in ( dom (F . k)) by A1, MESFUNC8:def 2;

        then

         A13: x in ( dom |.(F . k).|) by MESFUNC1:def 10;

        ( |.(F . k).| . x) <= (P . x) by A6, A12;

        then

         A14: |.((F . k) . x).| <= (P . x) by A13, MESFUNC1:def 10;

        then

         A15: ((F . k) . x) <= (P . x) by EXTREAL1: 23;

        ( - (P . x)) <= ((F . k) . x) by A14, EXTREAL1: 23;

        hence thesis by A15, MESFUNC5:def 13;

      end;

       A16:

      now

        let x be Element of X;

        assume

         A17: x in ( dom ( lim_inf F));

        now

          let k be Nat;

          

           A18: (( inferior_realsequence (F # x)) . k) <= ((F # x) . k) by RINFSUP2: 8;

          ((F # x) . k) <= (P . x) by A8, A11, A17;

          hence (( inferior_realsequence (F # x)) . k) <= (P . x) by A18, XXREAL_0: 2;

        end;

        then ( lim_inf (F # x)) <= (P . x) by Th5;

        then

         A19: (( lim_inf F) . x) <= (P . x) by A17, MESFUNC8:def 7;

        now

          let y be ExtReal;

          assume y in ( rng (F # x));

          then ex k be object st k in ( dom (F # x)) & y = ((F # x) . k) by FUNCT_1:def 3;

          hence ( - (P . x)) <= y by A8, A11, A17;

        end;

        then ( - (P . x)) is LowerBound of ( rng (F # x)) by XXREAL_2:def 2;

        then ( - (P . x)) <= ( inf ( rng (F # x))) by XXREAL_2:def 4;

        then ( - (P . x)) <= ( inf ((F # x) ^\ 0 )) by NAT_1: 47;

        then

         A20: ( - (P . x)) <= (( inferior_realsequence (F # x)) . 0 ) by RINFSUP2: 27;

        (( inferior_realsequence (F # x)) . 0 ) <= ( sup ( inferior_realsequence (F # x))) by RINFSUP2: 23;

        then ( - (P . x)) <= ( lim_inf (F # x)) by A20, XXREAL_0: 2;

        then ( - (P . x)) <= (( lim_inf F) . x) by A17, MESFUNC8:def 7;

        hence |.(( lim_inf F) . x).| <= (P . x) by A19, EXTREAL1: 23;

      end;

      ( lim_inf F) is E -measurable by A1, A3, MESFUNC8: 24;

      then ( lim_inf F) is_integrable_on M by A2, A4, A8, A16, MESFUNC5: 102;

      then

       A21: ex E3 be Element of S st E3 = (( dom P) /\ ( dom ( lim_inf F))) & ( Integral (M,(P + ( lim_inf F)))) = (( Integral (M,(P | E3))) + ( Integral (M,(( lim_inf F) | E3)))) by A4, MESFUNC5: 109;

      

       A22: (P | E) = P by A2, RELAT_1: 68;

      

       A23: ( Integral (M,P)) < +infty by A4, MESFUNC5: 96;

       -infty < ( Integral (M,P)) by A4, MESFUNC5: 96;

      then

       A24: ( Integral (M,P)) is Element of REAL by A23, XXREAL_0: 14;

      now

        let x be object;

        assume x in (P " { -infty });

        then

         A25: (P . x) in { -infty } by FUNCT_1:def 7;

         0 <= (P . x) by A5, SUPINF_2: 51;

        hence contradiction by A25, TARSKI:def 1;

      end;

      then

       A26: (P " { -infty }) = {} by XBOOLE_0:def 1;

       A27:

      now

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        then (G . n) = (P + (F . n)) by A10;

        hence (G . n) is PartFunc of X, ExtREAL ;

      end;

       A28:

      now

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        hence (G . n) = (P + (F . n)) by A10;

      end;

      reconsider G as Functional_Sequence of X, ExtREAL by A10, A27, SEQFUNC: 1;

      

       A29: (P " { +infty }) = {} by A7, MESFUNC5: 30;

      

       A30: for n be Nat holds ( dom (G . n)) = E

      proof

        let n be Nat;

        ( dom (G . n)) = ( dom (P + (F . n))) by A28;

        then

         A31: ( dom (G . n)) = ((( dom P) /\ ( dom (F . n))) \ (((P " { -infty }) /\ ((F . n) " { +infty })) \/ ((P " { +infty }) /\ ((F . n) " { -infty })))) by MESFUNC1:def 3;

        ( dom (F . n)) = E by A1, MESFUNC8:def 2;

        hence thesis by A2, A29, A26, A31;

      end;

       A32:

      now

        let n,m be Nat;

        

        thus ( dom (G . n)) = E by A30

        .= ( dom (G . m)) by A30;

      end;

      deffunc H( Nat) = (P - (F . $1));

      consider H be Function such that

       A33: ( dom H) = NAT & for n be Element of NAT holds (H . n) = H(n) from FUNCT_1:sch 4;

      reconsider G as with_the_same_dom Functional_Sequence of X, ExtREAL by A32, MESFUNC8:def 2;

      

       A34: ( dom (G . 0 )) = ( dom (F . 0 )) by A1, A30;

      

       A35: for n be Nat holds (F . n) is_integrable_on M

      proof

        let n be Nat;

        

         A36: E = ( dom (F . n)) by A1, MESFUNC8:def 2;

         A37:

        now

          let x be Element of X;

          assume

           A38: x in ( dom (F . n));

          then

           A39: x in ( dom |.(F . n).|) by MESFUNC1:def 10;

          ( |.(F . n).| . x) <= (P . x) by A6, A36, A38;

          hence |.((F . n) . x).| <= (P . x) by A39, MESFUNC1:def 10;

        end;

        (F . n) is E -measurable by A3;

        hence thesis by A2, A4, A36, A37, MESFUNC5: 102;

      end;

       A40:

      now

        let n be Nat;

        

         A41: (G . n) = (P + (F . n)) by A28;

        now

          let x be object;

          assume

           A42: x in ( dom (P + (F . n)));

          then

          reconsider x1 = x as Element of X;

          x in E by A30, A41, A42;

          then ( - (P . x)) <= ((F # x1) . n) by A11;

          then

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

          (( - (P . x)) + (P . x)) = 0 by XXREAL_3: 7;

          then 0 <= (((F . n) . x) + (P . x)) by A43, XXREAL_3: 36;

          hence 0 <= ((P + (F . n)) . x) by A42, MESFUNC1:def 3;

        end;

        hence (G . n) is nonnegative by A41, SUPINF_2: 52;

        (F . n) is_integrable_on M by A35;

        then (G . n) is_integrable_on M by A4, A41, MESFUNC5: 108;

        then

        consider E1 be Element of S such that

         AB: E1 = ( dom (G . n)) & (G . n) is E1 -measurable;

        for r be Real holds (E /\ ( less_dom ((G . n),r))) in S

        proof

          let r be Real;

          

           AC: (E1 /\ ( less_dom ((G . n),r))) in S by AB;

          E = E1 by A30, AB;

          hence thesis by AC;

        end;

        hence (G . n) is E -measurable;

      end;

      E = ( dom (G . 0 )) by A30;

      then

      consider IG be ExtREAL_sequence such that

       A44: for n be Nat holds (IG . n) = ( Integral (M,(G . n))) and

       A45: ( Integral (M,( lim_inf G))) <= ( lim_inf IG) by A40, Th7;

      

       A46: ( Integral (M,P)) < +infty by A4, MESFUNC5: 96;

      deffunc I( Nat) = ( Integral (M,(F . $1)));

      consider I be sequence of ExtREAL such that

       A47: for n be Element of NAT holds (I . n) = I(n) from FUNCT_2:sch 4;

      reconsider I as ExtREAL_sequence;

      

       A48: -infty < ( Integral (M,P)) by A4, MESFUNC5: 96;

      

       A49: for n be Nat holds (I . n) = ( Integral (M,(F . n))) & (I . n) in REAL

      proof

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        then

         A50: (I . n) = ( Integral (M,(F . n))) by A47;

        

         A51: (F . n) is_integrable_on M by A35;

        then

         A52: ( Integral (M,(F . n))) < +infty by MESFUNC5: 96;

         -infty < ( Integral (M,(F . n))) by A51, MESFUNC5: 96;

        hence thesis by A50, A52, XXREAL_0: 14;

      end;

      now

        let n be Nat;

        

         A53: (G . n) = (P + (F . n)) by A28;

        (F . n) is_integrable_on M by A35;

        then

         A54: ex E2 be Element of S st E2 = (( dom P) /\ ( dom (F . n))) & ( Integral (M,(G . n))) = (( Integral (M,(P | E2))) + ( Integral (M,((F . n) | E2)))) by A4, A53, MESFUNC5: 109;

        

         A55: (P | E) = P by A2, RELAT_1: 68;

        

         A56: ( dom (F . n)) = E by A1, MESFUNC8:def 2;

        then ((F . n) | E) = (F . n) by RELAT_1: 68;

        then ( Integral (M,(G . n))) = (( Integral (M,P)) + (I . n)) by A2, A49, A54, A56, A55;

        hence (IG . n) = (( Integral (M,P)) + (I . n)) by A44;

      end;

      then ( lim_inf IG) = (( Integral (M,P)) + ( lim_inf I)) by A24, Th10;

      then (( Integral (M,P)) + ( Integral (M,( lim_inf F)))) <= (( Integral (M,P)) + ( lim_inf I)) by A2, A8, A28, A29, A26, A45, A21, A22, A9, A34, Th11;

      then ( Integral (M,( lim_inf F))) <= ((( lim_inf I) + ( Integral (M,P))) - ( Integral (M,P))) by A48, A46, XXREAL_3: 56;

      then ( Integral (M,( lim_inf F))) <= (( lim_inf I) + (( Integral (M,P)) - ( Integral (M,P)))) by A48, A46, XXREAL_3: 30;

      then ( Integral (M,( lim_inf F))) <= (( lim_inf I) + 0. ) by XXREAL_3: 7;

      then

       A57: ( Integral (M,( lim_inf F))) <= ( lim_inf I) by XXREAL_3: 4;

       A58:

      now

        let n be Nat;

        

         A59: n in NAT by ORDINAL1:def 12;

        (H . n) = (P - (F . n)) by A33, A59;

        hence (H . n) is PartFunc of X, ExtREAL ;

      end;

       A60:

      now

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        hence (H . n) = (P - (F . n)) by A33;

      end;

      

       A61: E = ( dom ( lim_sup F)) by A1, MESFUNC8:def 8;

       A62:

      now

        let x be Element of X;

        assume

         A63: x in ( dom ( lim_sup F));

        for k be Nat holds (( superior_realsequence (F # x)) . k) >= ( - (P . x))

        proof

          let k be Nat;

          

           A64: (( superior_realsequence (F # x)) . k) >= ((F # x) . k) by RINFSUP2: 8;

          ((F # x) . k) >= ( - (P . x)) by A61, A11, A63;

          hence thesis by A64, XXREAL_0: 2;

        end;

        then ( lim_sup (F # x)) >= ( - (P . x)) by Th4;

        then

         A65: (( lim_sup F) . x) >= ( - (P . x)) by A63, MESFUNC8:def 8;

        now

          let y be ExtReal;

          assume y in ( rng (F # x));

          then ex k be object st k in ( dom (F # x)) & y = ((F # x) . k) by FUNCT_1:def 3;

          hence (P . x) >= y by A61, A11, A63;

        end;

        then (P . x) is UpperBound of ( rng (F # x)) by XXREAL_2:def 1;

        then (P . x) >= ( sup ( rng (F # x))) by XXREAL_2:def 3;

        then (P . x) >= ( sup ((F # x) ^\ 0 )) by NAT_1: 47;

        then

         A66: (P . x) >= (( superior_realsequence (F # x)) . 0 ) by RINFSUP2: 27;

        (( superior_realsequence (F # x)) . 0 ) >= ( inf ( superior_realsequence (F # x))) by RINFSUP2: 23;

        then (P . x) >= ( lim_sup (F # x)) by A66, XXREAL_0: 2;

        then (P . x) >= (( lim_sup F) . x) by A63, MESFUNC8:def 8;

        hence |.(( lim_sup F) . x).| <= (P . x) by A65, EXTREAL1: 23;

      end;

      ( lim_sup F) is E -measurable by A1, A3, MESFUNC8: 23;

      then

       A67: ( lim_sup F) is_integrable_on M by A2, A4, A61, A62, MESFUNC5: 102;

      then

       A68: ex E6 be Element of S st E6 = (( dom P) /\ ( dom ( lim_sup F))) & ( Integral (M,(P - ( lim_sup F)))) = (( Integral (M,(P | E6))) + ( Integral (M,(( - ( lim_sup F)) | E6)))) by A4, Th13;

      set E1 = ( Integral (M,( lim_sup F)));

      

       A69: E1 < +infty by A67, MESFUNC5: 96;

       -infty < E1 by A67, MESFUNC5: 96;

      then

      reconsider e1 = E1 as Element of REAL by A69, XXREAL_0: 14;

      

       A70: ( - E1) = ( - e1) by SUPINF_2: 2;

      

       A71: (P | E) = P by A2, RELAT_1: 68;

      deffunc F1( Nat) = ( - (F . $1));

      consider F1 be Function such that

       A72: ( dom F1) = NAT & for n be Element of NAT holds (F1 . n) = F1(n) from FUNCT_1:sch 4;

      reconsider H as Functional_Sequence of X, ExtREAL by A33, A58, SEQFUNC: 1;

       A73:

      now

        let n be Nat;

        

         A74: ( dom (H . n)) = ( dom (P - (F . n))) by A60;

        ( dom (F . n)) = E by A1, MESFUNC8:def 2;

        then ( dom (H . n)) = ((E /\ E) \ (( {} /\ ((F . n) " { +infty })) \/ ( {} /\ ((F . n) " { -infty })))) by A2, A29, A26, A74, MESFUNC1:def 4;

        hence ( dom (H . n)) = E;

      end;

      now

        let n,m be Nat;

        

        thus ( dom (H . n)) = E by A73

        .= ( dom (H . m)) by A73;

      end;

      then

      reconsider H as with_the_same_dom Functional_Sequence of X, ExtREAL by MESFUNC8:def 2;

      

       A75: -infty < ( Integral (M,P)) by A4, MESFUNC5: 96;

       A76:

      now

        let n be Nat;

        

         A77: (H . n) = (P - (F . n)) by A60;

        now

          let x be Element of X;

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

          then x in E by A1, MESFUNC8:def 2;

          then ((F # x) . n) <= (P . x) by A11;

          hence ((F . n) . x) <= (P . x) by MESFUNC5:def 13;

        end;

        hence (H . n) is nonnegative by A77, MESFUNC7: 1;

        (F . n) is_integrable_on M by A35;

        then (H . n) is_integrable_on M by A4, A77, Th12;

        then

        consider E4 be Element of S such that

         AA: E4 = ( dom (H . n)) & (H . n) is E4 -measurable;

        E4 = E by AA, A73;

        hence (H . n) is E -measurable by AA;

      end;

      E = ( dom (H . 0 )) by A73;

      then

      consider IH be ExtREAL_sequence such that

       A78: for n be Nat holds (IH . n) = ( Integral (M,(H . n))) and

       A79: ( Integral (M,( lim_inf H))) <= ( lim_inf IH) by A76, Th7;

      

       A80: ( Integral (M,P)) < +infty by A4, MESFUNC5: 96;

      now

        let n be Nat;

        

         A81: n in NAT by ORDINAL1:def 12;

        (F1 . n) = ( - (F . n)) by A72, A81;

        hence (F1 . n) is PartFunc of X, ExtREAL ;

      end;

      then

      reconsider F1 as Functional_Sequence of X, ExtREAL by A72, SEQFUNC: 1;

       A82:

      now

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        hence (F1 . n) = ( - (F . n)) by A72;

      end;

      now

        let n,m be Nat;

        (F1 . m) = ( - (F . m)) by A82;

        then

         A83: ( dom (F1 . m)) = ( dom (F . m)) by MESFUNC1:def 7;

        (F1 . n) = ( - (F . n)) by A82;

        then ( dom (F1 . n)) = ( dom (F . n)) by MESFUNC1:def 7;

        hence ( dom (F1 . n)) = ( dom (F1 . m)) by A83, MESFUNC8:def 2;

      end;

      then

      reconsider F1 as with_the_same_dom Functional_Sequence of X, ExtREAL by MESFUNC8:def 2;

      

       A84: ( Integral (M,( - ( lim_sup F)))) = ( Integral (M,(( - 1) (#) ( lim_sup F)))) by MESFUNC2: 9;

       A85:

      now

        let n be Nat;

        (H . n) = (P - (F . n)) by A60;

        then (H . n) = (P + ( - (F . n))) by MESFUNC2: 8;

        hence (H . n) = (P + (F1 . n)) by A82;

      end;

      (F1 . 0 ) = ( - (F . 0 )) by A82;

      then

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

      then ( dom (F1 . 0 )) = ( dom (H . 0 )) by A1, A73;

      then ( lim_inf H) = (P + ( lim_inf F1)) by A29, A26, A85, Th11;

      then ( lim_inf H) = (P + ( - ( lim_sup F))) by A82, A86, Th15;

      then

       A87: ( lim_inf H) = (P - ( lim_sup F)) by MESFUNC2: 8;

      E = ( dom ( lim_sup F)) by A1, MESFUNC8:def 8;

      then E = ( dom ( - ( lim_sup F))) by MESFUNC1:def 7;

      then

       A88: (( - ( lim_sup F)) | E) = ( - ( lim_sup F)) by RELAT_1: 68;

      deffunc I1( Nat) = ( - (I . $1));

      consider I1 be sequence of ExtREAL such that

       A89: for n be Element of NAT holds (I1 . n) = I1(n) from FUNCT_2:sch 4;

      reconsider I1 as ExtREAL_sequence;

       A90:

      now

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        hence (I1 . n) = ( - (I . n)) by A89;

      end;

      then

       A91: ( - ( lim_inf I1)) = ( lim_sup I) by Th14;

      now

        let n be Nat;

        

         A92: (F . n) is_integrable_on M by A35;

        ( Integral (M,( - (F . n)))) = ( Integral (M,(( - 1) (#) (F . n)))) by MESFUNC2: 9;

        then

         A93: ( Integral (M,( - (F . n)))) = (( - jj) * ( Integral (M,(F . n)))) by A92, MESFUNC5: 110;

        

         A94: ( dom (F . n)) = E by A1, MESFUNC8:def 2;

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

        then

         A95: (( - (F . n)) | E) = ( - (F . n)) by RELAT_1: 68;

        (H . n) = (P - (F . n)) by A60;

        then

         A96: ex E5 be Element of S st E5 = (( dom P) /\ ( dom (F . n))) & ( Integral (M,(H . n))) = (( Integral (M,(P | E5))) + ( Integral (M,(( - (F . n)) | E5)))) by A4, A92, Th13;

        reconsider In = (I . n) as Element of REAL by A49;

        

         A97: (( - 1) * (I . n)) = (( - 1) * In) by EXTREAL1: 1;

        

         A98: ( - (I . n)) = ( - In) by SUPINF_2: 2;

        (P | E) = P by A2, RELAT_1: 68;

        then ( Integral (M,(H . n))) = (( Integral (M,P)) + ( - (I . n))) by A2, A49, A96, A94, A95, A93, A97, A98;

        then (IH . n) = (( Integral (M,P)) + ( - (I . n))) by A78;

        hence (IH . n) = (( Integral (M,P)) + (I1 . n)) by A90;

      end;

      then ( lim_inf IH) = (( Integral (M,P)) + ( lim_inf I1)) by A24, Th10;

      then (( Integral (M,P)) + (( - jj) * ( Integral (M,( lim_sup F))))) <= (( Integral (M,P)) + ( - ( lim_sup I))) by A2, A61, A79, A91, A87, A67, A68, A71, A88, A84, MESFUNC5: 110;

      then (( - 1) * ( Integral (M,( lim_sup F)))) <= ((( - ( lim_sup I)) + ( Integral (M,P))) - ( Integral (M,P))) by A75, A80, XXREAL_3: 56;

      then (( - 1) * ( Integral (M,( lim_sup F)))) <= (( - ( lim_sup I)) + (( Integral (M,P)) - ( Integral (M,P)))) by A75, A80, XXREAL_3: 30;

      then

       A99: (( - 1) * ( Integral (M,( lim_sup F)))) <= (( - ( lim_sup I)) + 0. ) by XXREAL_3: 7;

      (( - 1) * E1) = (( - 1) * e1) by EXTREAL1: 1;

      then ( - ( Integral (M,( lim_sup F)))) <= ( - ( lim_sup I)) by A99, A70, XXREAL_3: 4;

      then

       A100: ( Integral (M,( lim_sup F))) >= ( lim_sup I) by XXREAL_3: 38;

      now

        

         A101: ( lim_inf I) <= ( lim_sup I) by RINFSUP2: 39;

        

         A102: ( dom ( lim F)) = ( dom (F . 0 )) by MESFUNC8:def 9;

        assume

         A103: for x be Element of X st x in E holds (F # x) is convergent;

        

         A104: for x be Element of X st x in ( dom ( lim F)) holds (( lim F) . x) = (( lim_inf F) . x)

        proof

          let x be Element of X;

          assume

           A105: x in ( dom ( lim F));

          then (F # x) is convergent by A1, A103, A102;

          hence thesis by A105, MESFUNC8: 14;

        end;

        

         A106: for x be Element of X st x in ( dom ( lim F)) holds (( lim F) . x) = (( lim_sup F) . x)

        proof

          let x be Element of X;

          assume

           A107: x in ( dom ( lim F));

          then (F # x) is convergent by A1, A103, A102;

          hence thesis by A107, MESFUNC8: 14;

        end;

        

         A108: ( dom ( lim F)) = ( dom ( lim_sup F)) by A102, MESFUNC8:def 8;

        then

         A109: ( lim F) = ( lim_sup F) by A106, PARTFUN1: 5;

        

         A110: ( dom ( lim F)) = ( dom ( lim_inf F)) by A102, MESFUNC8:def 7;

        then ( Integral (M,( lim F))) <= ( lim_inf I) by A57, A104, PARTFUN1: 5;

        then ( lim_sup I) <= ( lim_inf I) by A100, A109, XXREAL_0: 2;

        then ( lim_inf I) = ( lim_sup I) by A101, XXREAL_0: 1;

        hence

         A111: I is convergent by RINFSUP2: 40;

        then ( lim I) = ( lim_sup I) by RINFSUP2: 41;

        then

         A112: ( lim I) <= ( Integral (M,( lim F))) by A100, A108, A106, PARTFUN1: 5;

        ( lim I) = ( lim_inf I) by A111, RINFSUP2: 41;

        then ( Integral (M,( lim F))) <= ( lim I) by A57, A110, A104, PARTFUN1: 5;

        hence ( lim I) = ( Integral (M,( lim F))) by A112, XXREAL_0: 1;

      end;

      hence thesis by A49, A57, A100;

    end;

    theorem :: MESFUN10:17

    

     Th17: E = ( dom (F . 0 )) & E = ( dom P) & (for n be Nat holds (F . n) is E -measurable) & P is_integrable_on M & P is nonnegative & (for x be Element of X, n be Nat st x in E holds ( |.(F . n).| . x) <= (P . x)) implies ex I be ExtREAL_sequence st (for n be Nat holds (I . n) = ( Integral (M,(F . n)))) & ( lim_inf I) >= ( Integral (M,( lim_inf F))) & ( lim_sup I) <= ( Integral (M,( lim_sup F))) & ((for x be Element of X st x in E holds (F # x) is convergent) implies I is convergent & ( lim I) = ( Integral (M,( lim F))))

    proof

      assume that

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

       A2: E = ( dom P) and

       A3: for n be Nat holds (F . n) is E -measurable and

       A4: P is_integrable_on M and

       A5: P is nonnegative and

       A6: for x be Element of X, n be Nat st x in E holds ( |.(F . n).| . x) <= (P . x);

      for x be object st x in ( eq_dom (P, +infty )) holds x in E by A2, MESFUNC1:def 15;

      then ( eq_dom (P, +infty )) c= E by TARSKI:def 3;

      then

       A7: ( eq_dom (P, +infty )) = (E /\ ( eq_dom (P, +infty ))) by XBOOLE_1: 28;

      ex A be Element of S st A = ( dom P) & P is A -measurable by A4;

      then

      reconsider E0 = ( eq_dom (P, +infty )) as Element of S by A2, A7, MESFUNC1: 33;

      reconsider E1 = (E \ E0) as Element of S;

      deffunc F1( Nat) = ((F . $1) | E1);

      consider F1 be Functional_Sequence of X, ExtREAL such that

       A8: for n be Nat holds (F1 . n) = F1(n) from SEQFUNC:sch 1;

       A9:

      now

        let n be Nat;

        ( dom (F . n)) = E by A1, MESFUNC8:def 2;

        then ( dom ((F . n) | E1)) = E1 by RELAT_1: 62, XBOOLE_1: 36;

        hence ( dom (F1 . n)) = E1 by A8;

      end;

      then

       A10: E1 = ( dom (F1 . 0 ));

      now

        let n,m be Nat;

        

        thus ( dom (F1 . n)) = E1 by A9

        .= ( dom (F1 . m)) by A9;

      end;

      then

      reconsider F1 as with_the_same_dom Functional_Sequence of X, ExtREAL by MESFUNC8:def 2;

      set P1 = (P | E1);

      

       A11: P1 is nonnegative by A5, MESFUNC5: 15;

      

       A12: E1 c= E by XBOOLE_1: 36;

       A13:

      now

        let x be Element of X, n be Nat;

        assume

         A14: x in E1;

        then

         A15: (P1 . x) = (P . x) by FUNCT_1: 49;

        x in E by A12, A14;

        then x in ( dom (F . n)) by A1, MESFUNC8:def 2;

        then x in ( dom |.(F . n).|) by MESFUNC1:def 10;

        then

         A16: ( |.(F . n).| . x) = |.((F . n) . x).| by MESFUNC1:def 10;

        E1 = ( dom (F1 . n)) by A9;

        then

         A17: E1 = ( dom |.(F1 . n).|) by MESFUNC1:def 10;

        (F1 . n) = ((F . n) | E1) by A8;

        then ((F1 . n) . x) = ((F . n) . x) by A14, FUNCT_1: 49;

        then ( |.(F . n).| . x) = ( |.(F1 . n).| . x) by A14, A16, A17, MESFUNC1:def 10;

        hence ( |.(F1 . n).| . x) <= (P1 . x) by A6, A12, A14, A15;

      end;

      

       A18: ( dom ( lim F)) = ( dom (F . 0 )) by MESFUNC8:def 9;

      then

       A19: ( dom ( lim F)) = ( dom ( lim_inf F)) by MESFUNC8:def 7;

      

       A20: ( dom ( lim_inf F)) = E by A1, MESFUNC8:def 7;

       A21:

      now

        let x be Element of X;

        assume

         A22: x in ( dom ( lim_inf F1));

        then

         A23: x in E1 by A10, MESFUNC8:def 7;

        now

          let n be Element of NAT ;

          (((F . n) | E1) . x) = ((F . n) . x) by A23, FUNCT_1: 49;

          then ((F1 . n) . x) = ((F . n) . x) by A8;

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

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

        end;

        then

         A24: (F1 # x) = (F # x) by FUNCT_2: 63;

        E1 = ( dom ( lim_inf F1)) by A10, MESFUNC8:def 7;

        then ( lim_inf (F # x)) = (( lim_inf F) . x) by A12, A20, A22, MESFUNC8:def 7;

        then (( lim_inf F1) . x) = (( lim_inf F) . x) by A22, A24, MESFUNC8:def 7;

        hence ((( lim_inf F) | (E \ E0)) . x) = (( lim_inf F1) . x) by A23, FUNCT_1: 49;

      end;

      E1 = ( dom (( lim_inf F) | (E \ E0))) by A20, RELAT_1: 62, XBOOLE_1: 36;

      then ( dom (( lim_inf F) | (E \ E0))) = ( dom ( lim_inf F1)) by A10, MESFUNC8:def 7;

      then

       A25: (( lim_inf F) | (E \ E0)) = ( lim_inf F1) by A21, PARTFUN1: 5;

      

       A26: ( dom ( lim_sup F)) = E by A1, MESFUNC8:def 8;

       A27:

      now

        let x be Element of X;

        assume

         A28: x in ( dom ( lim_sup F1));

        then

         A29: x in E1 by A10, MESFUNC8:def 8;

        now

          let n be Element of NAT ;

          (((F . n) | E1) . x) = ((F . n) . x) by A29, FUNCT_1: 49;

          then ((F1 . n) . x) = ((F . n) . x) by A8;

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

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

        end;

        then

         A30: (F1 # x) = (F # x) by FUNCT_2: 63;

        E1 = ( dom ( lim_sup F1)) by A10, MESFUNC8:def 8;

        then ( lim_sup (F # x)) = (( lim_sup F) . x) by A12, A26, A28, MESFUNC8:def 8;

        then (( lim_sup F1) . x) = (( lim_sup F) . x) by A28, A30, MESFUNC8:def 8;

        hence ((( lim_sup F) | (E \ E0)) . x) = (( lim_sup F1) . x) by A29, FUNCT_1: 49;

      end;

      E1 = ( dom (( lim_sup F) | (E \ E0))) by A26, RELAT_1: 62, XBOOLE_1: 36;

      then ( dom (( lim_sup F) | (E \ E0))) = ( dom ( lim_sup F1)) by A10, MESFUNC8:def 8;

      then

       A31: (( lim_sup F) | (E \ E0)) = ( lim_sup F1) by A27, PARTFUN1: 5;

      

       A32: ( dom (P | E1)) = E1 by A2, RELAT_1: 62, XBOOLE_1: 36;

       A33:

      now

        assume ( eq_dom (P1, +infty )) <> {} ;

        then

        consider x be object such that

         A34: x in ( eq_dom (P1, +infty )) by XBOOLE_0:def 1;

        reconsider x as Element of X by A34;

        (P1 . x) = +infty by A34, MESFUNC1:def 15;

        then

        consider y be R_eal such that

         A35: y = (P1 . x) and

         A36: +infty = y;

        

         A37: x in E1 by A32, A34, MESFUNC1:def 15;

        then y = (P . x) by A35, FUNCT_1: 49;

        then x in ( eq_dom (P, +infty )) by A2, A12, A36, A37, MESFUNC1:def 15;

        hence contradiction by A37, XBOOLE_0:def 5;

      end;

      

       A38: for n be Nat holds (F1 . n) is E1 -measurable

      proof

        let n be Nat;

        ( dom (F . n)) = E by A1, MESFUNC8:def 2;

        then

         A39: E1 = (( dom (F . n)) /\ E1) by XBOOLE_1: 28, XBOOLE_1: 36;

        (F . n) is E -measurable by A3;

        then (F . n) is E1 -measurable by MESFUNC1: 30, XBOOLE_1: 36;

        then ((F . n) | E1) is E1 -measurable by A39, MESFUNC5: 42;

        hence thesis by A8;

      end;

      P1 is_integrable_on M by A4, MESFUNC5: 112;

      then

      consider I be ExtREAL_sequence such that

       A40: for n be Nat holds (I . n) = ( Integral (M,(F1 . n))) and

       A41: ( lim_inf I) >= ( Integral (M,( lim_inf F1))) and

       A42: ( lim_sup I) <= ( Integral (M,( lim_sup F1))) and (for x be Element of X st x in E1 holds (F1 # x) is convergent) implies I is convergent & ( lim I) = ( Integral (M,( lim F1))) by A32, A10, A11, A13, A38, A33, Lm1;

      (P " { +infty }) = E0 by MESFUNC5: 30;

      then

       A43: (M . E0) = 0 by A4, MESFUNC5: 105;

      

       A44: for n be Nat holds (I . n) = ( Integral (M,(F . n)))

      proof

        let n be Nat;

        

         A45: E = ( dom (F . n)) by A1, MESFUNC8:def 2;

        

         A46: (F . n) is E -measurable by A3;

         |.(F . n).| is_integrable_on M by A1, A2, A3, A4, A6, Th16;

        then (F . n) is_integrable_on M by A45, A46, MESFUNC5: 100;

        then ( Integral (M,(F . n))) = (( Integral (M,((F . n) | E0))) + ( Integral (M,((F . n) | E1)))) by A45, MESFUNC5: 99;

        then

         A47: ( Integral (M,(F . n))) = ( 0. + ( Integral (M,((F . n) | E1)))) by A3, A43, A45, MESFUNC5: 94;

        (I . n) = ( Integral (M,(F1 . n))) by A40;

        then (I . n) = ( Integral (M,((F . n) | E1))) by A8;

        hence thesis by A47, XXREAL_3: 4;

      end;

      ( lim_inf F) is E -measurable by A1, A3, MESFUNC8: 24;

      then

       A48: ( Integral (M,(( lim_inf F) | (E \ E0)))) = ( Integral (M,( lim_inf F))) by A43, A20, MESFUNC5: 95;

      ( lim_sup F) is E -measurable by A1, A3, MESFUNC8: 23;

      then

       A49: ( Integral (M,(( lim_sup F) | (E \ E0)))) = ( Integral (M,( lim_sup F))) by A43, A26, MESFUNC5: 95;

      

       A50: ( dom ( lim F)) = ( dom ( lim_sup F)) by A18, MESFUNC8:def 8;

      now

        assume

         A51: for x be Element of X st x in E holds (F # x) is convergent;

        

         A52: for x be Element of X st x in ( dom ( lim F)) holds (( lim F) . x) = (( lim_inf F) . x)

        proof

          let x be Element of X;

          assume

           A53: x in ( dom ( lim F));

          then (F # x) is convergent by A1, A18, A51;

          hence thesis by A53, MESFUNC8: 14;

        end;

        then

         A54: ( lim F) = ( lim_inf F) by A19, PARTFUN1: 5;

        

         A55: ( lim_inf I) <= ( lim_sup I) by RINFSUP2: 39;

        

         A56: for x be Element of X st x in ( dom ( lim F)) holds (( lim F) . x) = (( lim_sup F) . x)

        proof

          let x be Element of X;

          assume

           A57: x in ( dom ( lim F));

          then (F # x) is convergent by A1, A18, A51;

          hence thesis by A57, MESFUNC8: 14;

        end;

        then ( lim F) = ( lim_sup F) by A50, PARTFUN1: 5;

        then ( lim_sup I) <= ( lim_inf I) by A41, A42, A25, A31, A54, XXREAL_0: 2;

        then ( lim_inf I) = ( lim_sup I) by A55, XXREAL_0: 1;

        hence

         A58: I is convergent by RINFSUP2: 40;

        then ( lim I) = ( lim_sup I) by RINFSUP2: 41;

        then

         A59: ( lim I) <= ( Integral (M,( lim F))) by A42, A49, A31, A50, A56, PARTFUN1: 5;

        ( lim I) = ( lim_inf I) by A58, RINFSUP2: 41;

        then ( Integral (M,( lim F))) <= ( lim I) by A41, A48, A25, A19, A52, PARTFUN1: 5;

        hence ( lim I) = ( Integral (M,( lim F))) by A59, XXREAL_0: 1;

      end;

      hence thesis by A41, A42, A44, A48, A49, A25, A31;

    end;

    theorem :: MESFUN10:18

    E = ( dom (F . 0 )) & (for n holds (F . n) is nonnegative & (F . n) is E -measurable) & (for x, n, m st x in E & n <= m holds ((F . n) . x) >= ((F . m) . x)) & ( Integral (M,((F . 0 ) | E))) < +infty implies ex I be ExtREAL_sequence st (for n be Nat holds (I . n) = ( Integral (M,(F . n)))) & I is convergent & ( lim I) = ( Integral (M,( lim F)))

    proof

      assume that

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

       A2: for n holds (F . n) is nonnegative & (F . n) is E -measurable and

       A3: for x, n, m st x in E & n <= m holds ((F . n) . x) >= ((F . m) . x) and

       A4: ( Integral (M,((F . 0 ) | E))) < +infty ;

      

       A5: (F . 0 ) is nonnegative by A2;

      

       A6: ( dom (F . 0 )) = ( dom |.(F . 0 ).|) by MESFUNC1:def 10;

      

       A7: for x be Element of X st x in ( dom (F . 0 )) holds ((F . 0 ) . x) = ( |.(F . 0 ).| . x)

      proof

        let x be Element of X;

         0 <= ((F . 0 ) . x) by A5, SUPINF_2: 51;

        then

         A8: |.((F . 0 ) . x).| = ((F . 0 ) . x) by EXTREAL1:def 1;

        assume x in ( dom (F . 0 ));

        hence thesis by A6, A8, MESFUNC1:def 10;

      end;

      

       A9: (F . 0 ) is E -measurable by A2;

      then ( Integral (M,(F . 0 ))) = ( integral+ (M,(F . 0 ))) by A1, A5, MESFUNC5: 88;

      then ( integral+ (M,(F . 0 ))) < +infty by A1, A4, RELAT_1: 68;

      then

       A10: ( integral+ (M, |.(F . 0 ).|)) < +infty by A6, A7, PARTFUN1: 5;

      

       A11: ( max+ (F . 0 )) is E -measurable by A2, MESFUNC2: 25;

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

      then

       A12: ( max- (F . 0 )) is nonnegative by SUPINF_2: 52;

      

       A13: for x be Element of X, n be Nat st x in E holds ( |.(F . n).| . x) <= ((F . 0 ) . x)

      proof

        let x be Element of X, n be Nat;

        assume

         A14: x in E;

        (F . n) is nonnegative by A2;

        then 0 <= ((F . n) . x) by SUPINF_2: 51;

        then |.((F . n) . x).| = ((F . n) . x) by EXTREAL1:def 1;

        then

         A15: |.((F . n) . x).| <= ((F . 0 ) . x) by A3, A14;

        ( dom (F . n)) = ( dom |.(F . n).|) by MESFUNC1:def 10;

        then x in ( dom |.(F . n).|) by A1, A14, MESFUNC8:def 2;

        hence thesis by A15, MESFUNC1:def 10;

      end;

      

       A16: for x be Element of X st x in E holds (F # x) is convergent

      proof

        let x be Element of X;

        assume

         A17: x in E;

        now

          let n,m be Nat;

          assume m <= n;

          then ((F . n) . x) <= ((F . m) . x) by A3, A17;

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

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

        end;

        then (F # x) is non-increasing by RINFSUP2: 7;

        hence thesis by RINFSUP2: 36;

      end;

      

       A18: ( dom ( max+ (F . 0 ))) = ( dom (F . 0 )) by MESFUNC2:def 2;

      then

       A19: (( max+ (F . 0 )) | E) = ( max+ (F . 0 )) by A1, RELAT_1: 68;

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

      then

       A20: ( max+ (F . 0 )) is nonnegative by SUPINF_2: 52;

      then

       A21: ( dom (( max+ (F . 0 )) + ( max- (F . 0 )))) = (( dom ( max+ (F . 0 ))) /\ ( dom ( max- (F . 0 )))) by A12, MESFUNC5: 22;

      

       A22: ( dom ( max- (F . 0 ))) = ( dom (F . 0 )) by MESFUNC2:def 3;

      then

       A23: (( max- (F . 0 )) | E) = ( max- (F . 0 )) by A1, RELAT_1: 68;

      ( max- (F . 0 )) is E -measurable by A1, A2, MESFUNC2: 26;

      then ex C be Element of S st C = ( dom (( max+ (F . 0 )) + ( max- (F . 0 )))) & ( integral+ (M,(( max+ (F . 0 )) + ( max- (F . 0 ))))) = (( integral+ (M,(( max+ (F . 0 )) | C))) + ( integral+ (M,(( max- (F . 0 )) | C)))) by A1, A18, A22, A20, A12, A11, MESFUNC5: 78;

      then

       A24: (( integral+ (M,( max+ (F . 0 )))) + ( integral+ (M,( max- (F . 0 ))))) < +infty by A1, A18, A22, A21, A19, A23, A10, MESFUNC2: 24;

       0 <= ( integral+ (M,( max- (F . 0 )))) by A1, A9, A22, A12, MESFUNC2: 26, MESFUNC5: 79;

      then ( integral+ (M,( max+ (F . 0 )))) <> +infty by A24, XXREAL_3:def 2;

      then

       A25: ( integral+ (M,( max+ (F . 0 )))) < +infty by XXREAL_0: 4;

       0 <= ( integral+ (M,( max+ (F . 0 )))) by A1, A9, A18, A20, MESFUNC2: 25, MESFUNC5: 79;

      then ( integral+ (M,( max- (F . 0 )))) <> +infty by A24, XXREAL_3:def 2;

      then ( integral+ (M,( max- (F . 0 )))) < +infty by XXREAL_0: 4;

      then (F . 0 ) is_integrable_on M by A1, A9, A25;

      then ex I be ExtREAL_sequence st (for n be Nat holds (I . n) = ( Integral (M,(F . n)))) & ( lim_inf I) >= ( Integral (M,( lim_inf F))) & ( lim_sup I) <= ( Integral (M,( lim_sup F))) & ((for x be Element of X st x in E holds (F # x) is convergent) implies I is convergent & ( lim I) = ( Integral (M,( lim F)))) by A1, A2, A13, Th17;

      hence thesis by A16;

    end;

    definition

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

      :: MESFUN10:def1

      attr F is uniformly_bounded means ex K be Real st for n be Nat, x be set st x in ( dom (F . 0 )) holds |.((F . n) . x).| <= K;

    end

    ::$Notion-Name

    theorem :: MESFUN10:19

    (M . E) < +infty & E = ( dom (F . 0 )) & (for n be Nat holds (F . n) is E -measurable) & F is uniformly_bounded & (for x be Element of X st x in E holds (F # x) is convergent) implies (for n be Nat holds (F . n) is_integrable_on M) & ( lim F) is_integrable_on M & ex I be ExtREAL_sequence st (for n be Nat holds (I . n) = ( Integral (M,(F . n)))) & I is convergent & ( lim I) = ( Integral (M,( lim F)))

    proof

      assume that

       A1: (M . E) < +infty and

       A2: E = ( dom (F . 0 )) and

       A3: for n be Nat holds (F . n) is E -measurable and

       A4: F is uniformly_bounded and

       A5: for x be Element of X st x in E holds (F # x) is convergent;

      consider K1 be Real such that

       A6: for n be Nat, x be set st x in ( dom (F . 0 )) holds |.((F . n) . x).| <= K1 by A4;

      set K = ( max (K1,1));

      K in REAL by XREAL_0:def 1;

      then

      consider h be PartFunc of X, ExtREAL such that

       A7: h is_simple_func_in S and

       A8: ( dom h) = E and

       A9: for x be object st x in E holds (h . x) = K by MESFUNC5: 41, NUMBERS: 31;

      

       A10: ( dom h) = ( dom |.h.|) by MESFUNC1:def 10;

      

       A11: K > 0 by XXREAL_0: 30;

      then

       A12: (K * +infty ) = +infty by XXREAL_3:def 5;

      for x be object st x in E holds (h . x) >= 0. by A11, A9;

      then

       A13: h is nonnegative by A8, SUPINF_2: 52;

      then

       A14: ( Integral (M,h)) = ( integral' (M,h)) by A7, MESFUNC5: 89;

      

       A15: ( integral' (M,h)) = (K * (M . ( dom h))) by A11, A8, A9, MESFUNC5: 104;

      

       A16: for x be Element of X st x in ( dom h) holds (h . x) = ( |.h.| . x)

      proof

        let x be Element of X;

        assume x in ( dom h);

        then

         A17: x in ( dom |.h.|) by MESFUNC1:def 10;

         0 <= (h . x) by A13, SUPINF_2: 51;

        then |.(h . x).| = (h . x) by EXTREAL1:def 1;

        hence thesis by A17, MESFUNC1:def 10;

      end;

      ( Integral (M,h)) = ( integral+ (M,h)) by A7, A13, MESFUNC5: 89;

      then ( integral+ (M,h)) < +infty by A1, A11, A8, A15, A12, A14, XXREAL_3: 72;

      then

       A18: ( integral+ (M, |.h.|)) < +infty by A10, A16, PARTFUN1: 5;

      

       A19: ( dom ( max+ h)) = ( dom h) by MESFUNC2:def 2;

      then

       A20: (( max+ h) | E) = ( max+ h) by A8, RELAT_1: 68;

      

       A21: ( max+ h) is E -measurable by A7, MESFUNC2: 25, MESFUNC2: 34;

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

      then

       A22: ( max- h) is nonnegative by SUPINF_2: 52;

      

       A23: K >= K1 by XXREAL_0: 25;

      

       A24: for n be Nat, x be set st x in ( dom (F . 0 )) holds |.((F . n) . x).| <= K

      proof

        let n be Nat, x be set;

        assume x in ( dom (F . 0 ));

        then |.((F . n) . x).| <= K1 by A6;

        hence thesis by A23, XXREAL_0: 2;

      end;

      

       A25: for x be Element of X, n be Nat st x in E holds ( |.(F . n).| . x) <= (h . x)

      proof

        let x be Element of X, n be Nat;

        assume

         A26: x in E;

        ( dom (F . n)) = ( dom |.(F . n).|) by MESFUNC1:def 10;

        then x in ( dom |.(F . n).|) by A2, A26, MESFUNC8:def 2;

        then

         A27: ( |.(F . n).| . x) = |.((F . n) . x).| by MESFUNC1:def 10;

         |.((F . n) . x).| <= K by A2, A24, A26;

        hence thesis by A9, A26, A27;

      end;

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

      then

       A28: ( max+ h) is nonnegative by SUPINF_2: 52;

      then

       A29: ( dom (( max+ h) + ( max- h))) = (( dom ( max+ h)) /\ ( dom ( max- h))) by A22, MESFUNC5: 22;

      

       A30: ( dom ( max- h)) = ( dom h) by MESFUNC2:def 3;

      then

       A31: (( max- h) | E) = ( max- h) by A8, RELAT_1: 68;

      ( max- h) is E -measurable by A7, A8, MESFUNC2: 26, MESFUNC2: 34;

      then ex C be Element of S st C = ( dom (( max+ h) + ( max- h))) & ( integral+ (M,(( max+ h) + ( max- h)))) = (( integral+ (M,(( max+ h) | C))) + ( integral+ (M,(( max- h) | C)))) by A8, A19, A30, A21, A28, A22, MESFUNC5: 78;

      then

       A32: (( integral+ (M,( max+ h))) + ( integral+ (M,( max- h)))) < +infty by A8, A19, A30, A29, A20, A31, A18, MESFUNC2: 24;

      

       A33: for x be Element of X st x in ( dom ( lim F)) holds (( lim F) . x) = (( lim_inf F) . x)

      proof

        let x be Element of X;

        assume

         A34: x in ( dom ( lim F));

        then x in E by A2, MESFUNC8:def 9;

        then (F # x) is convergent by A5;

        hence thesis by A34, MESFUNC8: 14;

      end;

      

       A35: ( dom ( lim_inf F)) = ( dom (F . 0 )) by MESFUNC8:def 7;

      

       A36: h is E -measurable by A7, MESFUNC2: 34;

      then 0 <= ( integral+ (M,( max- h))) by A8, A30, A22, MESFUNC2: 26, MESFUNC5: 79;

      then ( integral+ (M,( max+ h))) <> +infty by A32, XXREAL_3:def 2;

      then

       A37: ( integral+ (M,( max+ h))) < +infty by XXREAL_0: 4;

       0 <= ( integral+ (M,( max+ h))) by A8, A36, A19, A28, MESFUNC2: 25, MESFUNC5: 79;

      then ( integral+ (M,( max- h))) <> +infty by A32, XXREAL_3:def 2;

      then ( integral+ (M,( max- h))) < +infty by XXREAL_0: 4;

      then

       A38: h is_integrable_on M by A8, A36, A37;

      then

       A39: ex I be ExtREAL_sequence st (for n be Nat holds (I . n) = ( Integral (M,(F . n)))) & ( lim_inf I) >= ( Integral (M,( lim_inf F))) & ( lim_sup I) <= ( Integral (M,( lim_sup F))) & ((for x be Element of X st x in E holds (F # x) is convergent) implies I is convergent & ( lim I) = ( Integral (M,( lim F)))) by A2, A3, A8, A13, A25, Th17;

       A40:

      now

        let n be Nat;

        

         A41: E = ( dom (F . n)) by A2, MESFUNC8:def 2;

        

         A42: (F . n) is E -measurable by A3;

         |.(F . n).| is_integrable_on M by A2, A3, A8, A38, A25, Th16;

        hence (F . n) is_integrable_on M by A41, A42, MESFUNC5: 100;

      end;

      

       A43: |.( lim_inf F).| is_integrable_on M by A2, A3, A8, A38, A25, Th16;

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

      then

       A44: ( lim F) = ( lim_inf F) by A35, A33, PARTFUN1: 5;

      then ( lim F) is E -measurable by A2, A3, MESFUNC8: 24;

      hence thesis by A2, A5, A43, A40, A35, A44, A39, MESFUNC5: 100;

    end;

    definition

      let X be set, F be Functional_Sequence of X, ExtREAL , f be PartFunc of X, ExtREAL ;

      :: MESFUN10:def2

      pred F is_uniformly_convergent_to f means F is with_the_same_dom & ( dom (F . 0 )) = ( dom f) & for e be Real st e > 0 holds ex N be Nat st for n be Nat, x be set st n >= N & x in ( dom (F . 0 )) holds |.(((F . n) . x) - (f . x)).| < e;

    end

    theorem :: MESFUN10:20

    

     Th20: F1 is_uniformly_convergent_to f implies for x be Element of X st x in ( dom (F1 . 0 )) holds (F1 # x) is convergent & ( lim (F1 # x)) = (f . x)

    proof

      assume

       A1: F1 is_uniformly_convergent_to f;

      let x be Element of X;

      assume

       A2: x in ( dom (F1 . 0 ));

      per cases by XXREAL_0: 14;

        suppose (f . x) in REAL ;

        then

        reconsider g = (f . x) as Real;

         A3:

        now

          let e be Real;

          assume 0 < e;

          then

          consider N be Nat such that

           A4: for n be Nat, x be set st n >= N & x in ( dom (F1 . 0 )) holds |.(((F1 . n) . x) - (f . x)).| < e by A1;

          take N;

          hereby

            let m be Nat;

            assume N <= m;

            then |.(((F1 . m) . x) - (f . x)).| < e by A2, A4;

            hence |.(((F1 # x) . m) - g).| < e by MESFUNC5:def 13;

          end;

        end;

        then

         A5: (F1 # x) is convergent_to_finite_number;

        then (F1 # x) is convergent;

        hence thesis by A3, A5, MESFUNC5:def 12;

      end;

        suppose

         A6: (f . x) = +infty ;

        now

          let e be Real;

          assume 0 < e;

          then

          consider N be Nat such that

           A7: for n be Nat, x be set st n >= N & x in ( dom (F1 . 0 )) holds |.(((F1 . n) . x) - (f . x)).| < e by A1;

          take N;

          hereby

            let n be Nat;

            assume n >= N;

            then |.(((F1 . n) . x) - (f . x)).| < e by A2, A7;

            then

             A8: |.( - (((F1 . n) . x) - (f . x))).| < e by EXTREAL1: 29;

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

            then ( - (((F1 # x) . n) - (f . x))) < e by A8, EXTREAL1: 21;

            then ((f . x) - ((F1 # x) . n)) < e by XXREAL_3: 26;

            then ((F1 # x) . n) = +infty by A6, XXREAL_3: 54;

            hence e <= ((F1 # x) . n) by XXREAL_0: 3;

          end;

        end;

        then

         A9: (F1 # x) is convergent_to_+infty;

        then (F1 # x) is convergent;

        hence thesis by A6, A9, MESFUNC5:def 12;

      end;

        suppose

         A10: (f . x) = -infty ;

        now

          let e be Real;

          assume e < 0 ;

          then ( - 0 ) < ( - e) by XREAL_1: 24;

          then

          consider N be Nat such that

           A11: for n be Nat, x be set st n >= N & x in ( dom (F1 . 0 )) holds |.(((F1 . n) . x) - (f . x)).| < ( - e) by A1;

          take N;

          hereby

            let n be Nat;

            assume n >= N;

            then

             A12: |.(((F1 . n) . x) - (f . x)).| < ( - e) by A2, A11;

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

            then (((F1 # x) . n) - (f . x)) < ( - e) by A12, EXTREAL1: 21;

            then ((F1 # x) . n) = -infty by A10, XXREAL_3: 54;

            hence e >= ((F1 # x) . n) by XXREAL_0: 5;

          end;

        end;

        then

         A13: (F1 # x) is convergent_to_-infty;

        then (F1 # x) is convergent;

        hence thesis by A10, A13, MESFUNC5:def 12;

      end;

    end;

    theorem :: MESFUN10:21

    (M . E) < +infty & E = ( dom (F . 0 )) & (for n be Nat holds (F . n) is_integrable_on M) & F is_uniformly_convergent_to f implies f is_integrable_on M & ex I be ExtREAL_sequence st (for n be Nat holds (I . n) = ( Integral (M,(F . n)))) & I is convergent & ( lim I) = ( Integral (M,f))

    proof

      assume that

       A1: (M . E) < +infty and

       A2: E = ( dom (F . 0 )) and

       A3: for n be Nat holds (F . n) is_integrable_on M and

       A4: F is_uniformly_convergent_to f;

      reconsider e = (1 / 2) as Real;

      consider N be Nat such that

       A5: for n be Nat, x be set st n >= N & x in ( dom (F . 0 )) holds |.(((F . n) . x) - (f . x)).| < e by A4;

      reconsider N1 = N as Nat;

      consider h be PartFunc of X, ExtREAL such that

       A6: h is_simple_func_in S and

       A7: ( dom h) = E and

       A8: for x be object st x in E holds (h . x) = 1. by MESFUNC5: 41;

      

       A9: ( max- h) is E -measurable by A6, A7, MESFUNC2: 26, MESFUNC2: 34;

      for x be object st x in E holds (h . x) >= 0. by A8;

      then

       A10: h is nonnegative by A7, SUPINF_2: 52;

      then

       A11: ( Integral (M,h)) = ( integral' (M,h)) by A6, MESFUNC5: 89;

      set AFN = |.(F . N).|;

      

       A12: ( dom (F . N)) = ( dom AFN) by MESFUNC1:def 10;

      now

        let x be object;

        assume x in ( dom AFN);

        then (AFN . x) = |.((F . N) . x).| by MESFUNC1:def 10;

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

      end;

      then

       A13: AFN is nonnegative by SUPINF_2: 52;

      then

       A14: ( dom (AFN + h)) = (( dom AFN) /\ ( dom h)) by A10, MESFUNC5: 22;

      

       A15: for x be set st x in ( dom (F . 0 )) holds |.(((F . N) . x) - (f . x)).| < (1 / 2) by A5;

       A16:

      now

        let x be set, n be Nat;

        assume that

         A17: n >= N and

         A18: x in ( dom (F . 0 ));

        

         A19: |.(((F . n) . x) - (f . x)).| < (jj / 2) by A5, A17, A18;

        

         A20: |.(((F . N) . x) - (f . x)).| < (jj / 2) by A5, A18;

         A21:

        now

          

           A22: |.(((F . n) . x) - (f . x)).| < 1 by A19, XXREAL_0: 2;

          then

           A23: (((F . n) . x) - (f . x)) < 1. by EXTREAL1: 21;

          

           A24: |.(((F . N) . x) - (f . x)).| < 1 by A20, XXREAL_0: 2;

          then

           A25: ( - 1. ) < (((F . N) . x) - (f . x)) by EXTREAL1: 21;

          

           A26: (((F . N) . x) - (f . x)) < 1. by A24, EXTREAL1: 21;

          assume

           A27: (f . x) = +infty or (f . x) = -infty ;

          ( - 1. ) < (((F . n) . x) - (f . x)) by A22, EXTREAL1: 21;

          then ((F . n) . x) = +infty & ((F . N) . x) = +infty or ((F . n) . x) = -infty & ((F . N) . x) = -infty by A27, A25, A23, A26, XXREAL_3: 53, XXREAL_3: 54;

          hence |.((F . n) . x).| <= ( |.((F . N) . x).| + 1. ) by EXTREAL1: 30, XXREAL_3: 52;

        end;

        ( dom (AFN + h)) = (( dom AFN) /\ ( dom h)) by A10, A13, MESFUNC5: 22;

        then ( dom (AFN + h)) = (E /\ E) by A2, A7, A12, MESFUNC8:def 2;

        then ((AFN . x) + (h . x)) = ((AFN + h) . x) by A2, A18, MESFUNC1:def 3;

        then

         A28: ((AFN . x) + 1. ) = ((AFN + h) . x) by A2, A8, A18;

        ( dom (F . n)) = E by A2, MESFUNC8:def 2;

        then

         A29: x in ( dom |.(F . n).|) by A2, A18, MESFUNC1:def 10;

         A30:

        now

          

           A31: 0 <= |.(((F . n) . x) - (f . x)).| by EXTREAL1: 14;

          

           A32: (jj / 2) in REAL by XREAL_0:def 1;

          then |.(((F . n) . x) - (f . x)).| < +infty by A19, XXREAL_0: 2, XXREAL_0: 9;

          then

          reconsider a = |.(((F . n) . x) - (f . x)).| as Element of REAL by A31, XXREAL_0: 14;

           |.((f . x) - ((F . N) . x)).| < (jj / 2) by A20, MESFUNC5: 1;

          then

           A33: |.((f . x) - ((F . N) . x)).| < +infty by XXREAL_0: 2, XXREAL_0: 9, A32;

           0 <= |.((f . x) - ((F . N) . x)).| by EXTREAL1: 14;

          then

          reconsider b = |.((f . x) - ((F . N) . x)).| as Element of REAL by A33, XXREAL_0: 14;

          assume

           A34: (f . x) in REAL ;

           A35:

          now

            assume ((F . N) . x) = +infty or ((F . N) . x) = -infty ;

            then (((F . N) . x) - (f . x)) = +infty or (((F . N) . x) - (f . x)) = -infty by A34, XXREAL_3: 13, XXREAL_3: 14;

            then jj < |.(((F . N) . x) - (f . x)).| by EXTREAL1: 30, XXREAL_0: 9;

            hence contradiction by A15, A18, XXREAL_0: 2;

          end;

           A36:

          now

            assume ((F . n) . x) = +infty or ((F . n) . x) = -infty ;

            then (((F . n) . x) - (f . x)) = +infty or (((F . n) . x) - (f . x)) = -infty by A34, XXREAL_3: 13, XXREAL_3: 14;

            hence contradiction by A19, EXTREAL1: 30, XXREAL_0: 9, A32;

          end;

          then ((F . n) . x) in REAL by XXREAL_0: 14;

          then

           A37: ( |.((F . n) . x).| - |.((F . N) . x).|) <= |.(((F . n) . x) - ((F . N) . x)).| by EXTREAL1: 31;

          b <= (1 / 2) by A20, MESFUNC5: 1;

          then (a + b) < ((1 / 2) + (1 / 2)) by A19, XREAL_1: 8;

          then

           A38: ( |.(((F . n) . x) - (f . x)).| + |.((f . x) - ((F . N) . x)).|) < 1 by SUPINF_2: 1;

          (( - (f . x)) + (f . x)) = 0. by XXREAL_3: 7;

          then (((F . n) . x) - ((F . N) . x)) = ((((F . n) . x) + (( - (f . x)) + (f . x))) - ((F . N) . x)) by XXREAL_3: 4;

          then (((F . n) . x) - ((F . N) . x)) = (((((F . n) . x) + ( - (f . x))) + (f . x)) - ((F . N) . x)) by A34, A36, XXREAL_3: 29;

          then (((F . n) . x) - ((F . N) . x)) = ((((F . n) . x) - (f . x)) + ((f . x) - ((F . N) . x))) by A34, A35, XXREAL_3: 30;

          then |.(((F . n) . x) - ((F . N) . x)).| <= ( |.(((F . n) . x) - (f . x)).| + |.((f . x) - ((F . N) . x)).|) by EXTREAL1: 24;

          then |.(((F . n) . x) - ((F . N) . x)).| < 1 by A38, XXREAL_0: 2;

          then ( |.((F . n) . x).| - |.((F . N) . x).|) <= 1. by A37, XXREAL_0: 2;

          hence |.((F . n) . x).| <= ( |.((F . N) . x).| + 1. ) by XXREAL_3: 52;

        end;

        x in ( dom AFN) by A12, A18, MESFUNC8:def 2;

        then |.((F . n) . x).| <= ((AFN . x) + 1. ) by A30, A21, MESFUNC1:def 10, XXREAL_0: 14;

        hence ( |.(F . n).| . x) <= ((AFN + h) . x) by A28, A29, MESFUNC1:def 10;

      end;

      

       A39: for x be Element of X, n be Nat st x in E holds ( |.((F ^\ N1) . n).| . x) <= ((AFN + h) . x)

      proof

        let x be Element of X, n be Nat;

        

         A40: ((F ^\ N1) . n) = (F . (n + N)) by NAT_1:def 3;

        assume x in E;

        hence thesis by A2, A16, A40, NAT_1: 11;

      end;

      

       A41: ( max+ h) is E -measurable by A6, MESFUNC2: 25, MESFUNC2: 34;

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

      then

       A42: ( max- h) is nonnegative by SUPINF_2: 52;

      

       A43: for n be Nat holds (F . n) is E -measurable

      proof

        let n be Nat;

        (F . n) is_integrable_on M by A3;

        then

        consider A be Element of S such that

         AA: A = ( dom (F . n)) & (F . n) is A -measurable;

        for r be Real holds (E /\ ( less_dom ((F . n),r))) in S

        proof

          let r be Real;

          E = ( dom (F . n)) by A2, MESFUNC8:def 2;

          then E = A by AA;

          hence thesis by AA;

        end;

        hence thesis;

      end;

      ((F ^\ N1) . 0 ) = (F . ( 0 + N)) by NAT_1:def 3;

      then

       A45: ( dom ((F ^\ N1) . 0 )) = E by A2, MESFUNC8:def 2;

       A46:

      now

        let x be Element of X;

        assume x in ( dom f);

        then

         A47: x in ( dom (F . 0 )) by A4;

        then

         A48: x in ( dom ( lim F)) by MESFUNC8:def 9;

        ( lim (F # x)) = (f . x) by A4, A47, Th20;

        hence (( lim F) . x) = (f . x) by A48, MESFUNC8:def 9;

      end;

      ( dom f) = ( dom (F . 0 )) by A4;

      then ( dom ( lim F)) = ( dom f) by MESFUNC8:def 9;

      then

       A49: ( lim F) = f by A46, PARTFUN1: 5;

      (F . N) is_integrable_on M by A3;

      then

       A51: AFN is_integrable_on M by MESFUNC5: 100;

      deffunc I( Nat) = ( Integral (M,(F . $1)));

      

       A52: (1 * +infty ) = +infty by XXREAL_3:def 5;

       A53:

      now

        let x be Element of X;

        assume x in ( dom h);

        then

         A54: x in ( dom |.h.|) by MESFUNC1:def 10;

         0 <= (h . x) by A10, SUPINF_2: 51;

        then |.(h . x).| = (h . x) by EXTREAL1:def 1;

        hence ( |.h.| . x) = (h . x) by A54, MESFUNC1:def 10;

      end;

      ( dom h) = ( dom |.h.|) by MESFUNC1:def 10;

      then

       A55: h = |.h.| by A53, PARTFUN1: 5;

      ( Integral (M,h)) = ( integral+ (M,h)) by A6, A10, MESFUNC5: 89;

      then ( integral+ (M,h)) = (jj * (M . ( dom h))) by A7, A8, A11, MESFUNC5: 104;

      then

       A56: ( integral+ (M, |.h.|)) < +infty by A1, A7, A55, A52, XXREAL_3: 72;

      

       A57: for n be Nat holds ((F ^\ N1) . n) is E -measurable

      proof

        let n be Nat;

        ((F ^\ N1) . n) = (F . (n + N)) by NAT_1:def 3;

        hence thesis by A43;

      end;

      

       A58: for x be Element of X st x in E holds ((F ^\ N1) # x) is convergent & ( lim (F # x)) = ( lim ((F ^\ N1) # x))

      proof

        let x be Element of X;

         A59:

        now

          let n be Element of NAT ;

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

          then (((F ^\ N1) # x) . n) = ((F . (n + N)) . x) by NAT_1:def 3;

          then (((F ^\ N1) # x) . n) = ((F # x) . (n + N)) by MESFUNC5:def 13;

          hence (((F ^\ N1) # x) . n) = (((F # x) ^\ N1) . n) by NAT_1:def 3;

        end;

        assume x in E;

        then

         A60: (F # x) is convergent by A2, A4, Th20;

        then ((F # x) ^\ N1) is convergent by RINFSUP2: 21;

        hence ((F ^\ N1) # x) is convergent by A59, FUNCT_2: 63;

        ( lim (F # x)) = ( lim ((F # x) ^\ N1)) by A60, RINFSUP2: 21;

        hence thesis by A59, FUNCT_2: 63;

      end;

      then for x be Element of X st x in E holds ((F ^\ N1) # x) is convergent;

      then

       A61: ( lim (F ^\ N1)) is E -measurable by A57, A45, MESFUNC8: 25;

      ( dom ( lim (F ^\ N1))) = E by A45, MESFUNC8:def 9;

      then

       A62: ( dom ( lim F)) = ( dom ( lim (F ^\ N1))) by A2, MESFUNC8:def 9;

       A63:

      now

        let x be Element of X;

        assume

         A64: x in ( dom ( lim F));

        then x in E by A2, MESFUNC8:def 9;

        then

         A65: ( lim (F # x)) = ( lim ((F ^\ N1) # x)) by A58;

        ( lim ((F ^\ N1) # x)) = (( lim (F ^\ N1)) . x) by A62, A64, MESFUNC8:def 9;

        hence (( lim F) . x) = (( lim (F ^\ N1)) . x) by A64, A65, MESFUNC8:def 9;

      end;

      

       A66: ( dom ( max- h)) = ( dom h) by MESFUNC2:def 3;

      then

       A67: (( max- h) | E) = ( max- h) by A7, RELAT_1: 68;

      

       A68: ( dom ( max+ h)) = ( dom h) by MESFUNC2:def 2;

      then

       A69: (( max+ h) | E) = ( max+ h) by A7, RELAT_1: 68;

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

      then

       A70: ( max+ h) is nonnegative by SUPINF_2: 52;

      then ( dom (( max+ h) + ( max- h))) = (( dom ( max+ h)) /\ ( dom ( max- h))) by A42, MESFUNC5: 22;

      then ex C be Element of S st C = E & ( integral+ (M,(( max+ h) + ( max- h)))) = (( integral+ (M,(( max+ h) | C))) + ( integral+ (M,(( max- h) | C)))) by A7, A41, A9, A70, A42, A68, A66, MESFUNC5: 78;

      then

       A71: ( integral+ (M, |.h.|)) = (( integral+ (M,( max+ h))) + ( integral+ (M,( max- h)))) by A69, A67, MESFUNC2: 24;

      

       A72: h is E -measurable by A6, MESFUNC2: 34;

      then 0 <= ( integral+ (M,( max- h))) by A7, A42, A66, MESFUNC2: 26, MESFUNC5: 79;

      then ( integral+ (M,( max+ h))) <> +infty by A71, A56, XXREAL_3:def 2;

      then

       A73: ( integral+ (M,( max+ h))) < +infty by XXREAL_0: 4;

       0 <= ( integral+ (M,( max+ h))) by A7, A72, A70, A68, MESFUNC2: 25, MESFUNC5: 79;

      then ( integral+ (M,( max- h))) <> +infty by A71, A56, XXREAL_3:def 2;

      then ( integral+ (M,( max- h))) < +infty by XXREAL_0: 4;

      then h is_integrable_on M by A7, A72, A73;

      then

       A74: (AFN + h) is_integrable_on M by A51, MESFUNC5: 108;

      

       A75: E = ( dom AFN) by A2, A12, MESFUNC8:def 2;

      then

       A76: |.( lim_inf (F ^\ N1)).| is_integrable_on M by A7, A74, A14, A39, A57, A45, Th16;

      (AFN + h) is nonnegative by A10, A13, MESFUNC5: 22;

      then

      consider J be ExtREAL_sequence such that

       A77: for n be Nat holds (J . n) = ( Integral (M,((F ^\ N1) . n))) and ( lim_inf J) >= ( Integral (M,( lim_inf (F ^\ N1)))) and ( lim_sup J) <= ( Integral (M,( lim_sup (F ^\ N1)))) and

       A78: (for x be Element of X st x in E holds ((F ^\ N1) # x) is convergent) implies J is convergent & ( lim J) = ( Integral (M,( lim (F ^\ N1)))) by A7, A74, A14, A75, A39, A57, A45, Th17;

      consider I be sequence of ExtREAL such that

       A79: for n be Element of NAT holds (I . n) = I(n) from FUNCT_2:sch 4;

      reconsider I as ExtREAL_sequence;

      

       A80: ( dom ( lim_inf (F ^\ N1))) = ( dom ((F ^\ N1) . 0 )) by MESFUNC8:def 7;

       A81:

      now

        let x be Element of X;

        assume

         A82: x in ( dom ( lim (F ^\ N1)));

        then x in E by A45, MESFUNC8:def 9;

        then ((F ^\ N1) # x) is convergent by A58;

        hence (( lim (F ^\ N1)) . x) = (( lim_inf (F ^\ N1)) . x) by A82, MESFUNC8: 14;

      end;

      ( dom ( lim (F ^\ N1))) = ( dom ((F ^\ N1) . 0 )) by MESFUNC8:def 9;

      then ( lim (F ^\ N1)) = ( lim_inf (F ^\ N1)) by A80, A81, PARTFUN1: 5;

      then

       A83: ( lim (F ^\ N1)) is_integrable_on M by A45, A76, A80, A61, MESFUNC5: 100;

      

       A84: for n be Nat holds (I . n) = ( Integral (M,(F . n)))

      proof

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A79;

      end;

      now

        let n be Element of NAT ;

        

         A85: ((F ^\ N1) . n) = (F . (n + N)) by NAT_1:def 3;

        

         A86: ((I ^\ N1) . n) = (I . (n + N)) by NAT_1:def 3;

        reconsider nn = (n + N) as Element of NAT by ORDINAL1:def 12;

        

        thus (J . n) = ( Integral (M,((F ^\ N1) . n))) by A77

        .= (I . nn) by A79, A85

        .= ((I ^\ N1) . n) by A86;

      end;

      then

       A87: J = (I ^\ N1) by FUNCT_2: 63;

      then

       A88: I is convergent by A58, A78, RINFSUP2: 17;

      ( lim I) = ( lim J) by A58, A78, A87, RINFSUP2: 17;

      then ( lim I) = ( Integral (M,( lim F))) by A58, A62, A63, A78, PARTFUN1: 5;

      hence thesis by A49, A62, A63, A83, A84, A88, PARTFUN1: 5;

    end;