mesfunc9.miz



    begin

    reserve X for non empty set,

S for SigmaField of X,

M for sigma_Measure of S,

E for Element of S,

F,G for Functional_Sequence of X, ExtREAL ,

I for ExtREAL_sequence,

f,g for PartFunc of X, ExtREAL ,

seq,seq1,seq2 for ExtREAL_sequence,

p for ExtReal,

n,m for Nat,

x for Element of X,

z,D for set;

    theorem :: MESFUNC9:1

    f is without+infty & g is without+infty implies ( dom (f + g)) = (( dom f) /\ ( dom g))

    proof

      assume that

       A1: f is without+infty and

       A2: g is without+infty;

       not +infty in ( rng g) by A2;

      then

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

       not +infty in ( rng f) by A1;

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

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

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

      hence thesis;

    end;

    theorem :: MESFUNC9:2

    f is without+infty & g is without-infty implies ( dom (f - g)) = (( dom f) /\ ( dom g))

    proof

      assume that

       A1: f is without+infty and

       A2: g is without-infty;

       not +infty in ( rng f) by A1;

      then

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

       not -infty in ( rng g) by A2;

      then (g " { -infty }) = {} by FUNCT_1: 72;

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

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

      hence thesis;

    end;

    theorem :: MESFUNC9:3

    

     Th3: f is without-infty & g is without-infty implies (f + g) is without-infty

    proof

      assume that

       A1: f is without-infty and

       A2: g is without-infty;

      for x be set st x in ( dom (f + g)) holds -infty < ((f + g) . x)

      proof

        let x be set;

        assume

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

        

         A4: -infty < (f . x) by A1;

        

         A5: -infty < (g . x) by A2;

        ((f + g) . x) = ((f . x) + (g . x)) by A3, MESFUNC1:def 3;

        hence thesis by A4, A5, XXREAL_0: 6, XXREAL_3: 17;

      end;

      hence thesis by MESFUNC5: 10;

    end;

    theorem :: MESFUNC9:4

    

     Th4: f is without+infty & g is without+infty implies (f + g) is without+infty

    proof

      assume that

       A1: f is without+infty and

       A2: g is without+infty;

      for x be set st x in ( dom (f + g)) holds ((f + g) . x) < +infty

      proof

        let x be set;

        assume

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

        

         A4: (f . x) < +infty by A1;

        

         A5: (g . x) < +infty by A2;

        ((f + g) . x) = ((f . x) + (g . x)) by A3, MESFUNC1:def 3;

        hence thesis by A4, A5, XXREAL_0: 4, XXREAL_3: 16;

      end;

      hence thesis by MESFUNC5: 11;

    end;

    theorem :: MESFUNC9:5

    f is without-infty & g is without+infty implies (f - g) is without-infty

    proof

      assume that

       A1: f is without-infty and

       A2: g is without+infty;

      for x be set st x in ( dom (f - g)) holds -infty < ((f - g) . x)

      proof

        let x be set;

        assume

         A3: x in ( dom (f - g));

        

         A4: -infty < (f . x) by A1;

        

         A5: (g . x) < +infty by A2;

        ((f - g) . x) = ((f . x) - (g . x)) by A3, MESFUNC1:def 4;

        hence thesis by A4, A5, XXREAL_0: 6, XXREAL_3: 19;

      end;

      hence thesis by MESFUNC5: 10;

    end;

    theorem :: MESFUNC9:6

    f is without+infty & g is without-infty implies (f - g) is without+infty

    proof

      assume that

       A1: f is without+infty and

       A2: g is without-infty;

      for x be set st x in ( dom (f - g)) holds ((f - g) . x) < +infty

      proof

        let x be set;

        assume

         A3: x in ( dom (f - g));

        

         A4: (f . x) < +infty by A1;

        

         A5: -infty < (g . x) by A2;

        ((f - g) . x) = ((f . x) - (g . x)) by A3, MESFUNC1:def 4;

        hence thesis by A4, A5, XXREAL_0: 4, XXREAL_3: 18;

      end;

      hence thesis by MESFUNC5: 11;

    end;

    theorem :: MESFUNC9:7

    

     Th7: (seq is convergent_to_finite_number implies ex g be Real st ( lim seq) = g & for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((seq . m) - ( lim seq)).| < p) & (seq is convergent_to_+infty implies ( lim seq) = +infty ) & (seq is convergent_to_-infty implies ( lim seq) = -infty )

    proof

       A1:

      now

        assume

         A2: seq is convergent_to_finite_number;

        then

         A3: not seq is convergent_to_+infty by MESFUNC5: 50;

        

         A4: not seq is convergent_to_-infty by A2, MESFUNC5: 51;

        seq is convergent by A2;

        then

        consider g be Real such that

         A5: ( lim seq) = g and

         A6: for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((seq . m) - ( lim seq)).| < p and seq is convergent_to_finite_number by A3, A4, MESFUNC5:def 12;

        take g;

        thus ex g be Real st ( lim seq) = g & for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((seq . m) - ( lim seq)).| < p by A5, A6;

      end;

       A7:

      now

        assume

         A8: seq is convergent_to_-infty;

        then seq is convergent;

        hence ( lim seq) = -infty by A8, MESFUNC5:def 12;

      end;

      now

        assume

         A9: seq is convergent_to_+infty;

        then seq is convergent;

        hence ( lim seq) = +infty by A9, MESFUNC5:def 12;

      end;

      hence thesis by A1, A7;

    end;

    theorem :: MESFUNC9:8

    

     Th8: seq is nonnegative implies not seq is convergent_to_-infty

    proof

      assume

       A1: seq is nonnegative;

      assume seq is convergent_to_-infty;

      then

      consider n be Nat such that

       A2: for m be Nat st n <= m holds (seq . m) <= ( - 1);

      (seq . n) <= ( - 1) by A2;

      hence contradiction by A1, SUPINF_2: 51;

    end;

    theorem :: MESFUNC9:9

    

     Th9: seq is convergent & (for k be Nat holds (seq . k) <= p) implies ( lim seq) <= p

    proof

      assume that

       A1: seq is convergent and

       A2: for k be Nat holds (seq . k) <= p;

      for y be ExtReal holds y in ( rng seq) implies y <= p

      proof

        let y be ExtReal;

        assume y in ( rng seq);

        then

        consider x be object such that

         A3: x in ( dom seq) and

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

        reconsider x as Nat by A3;

        (seq . x) <= p by A2;

        hence thesis by A4;

      end;

      then

       A5: p is UpperBound of ( rng seq) by XXREAL_2:def 1;

      reconsider SUPSEQ = ( superior_realsequence seq) as sequence of ExtREAL ;

      consider Y be non empty Subset of ExtREAL such that

       A6: Y = { (seq . k) where k be Nat : 0 <= k } and

       A7: (SUPSEQ . 0 ) = ( sup Y) by RINFSUP2:def 7;

      now

        let x be object;

        assume x in ( rng seq);

        then

        consider k be object such that

         A8: k in ( dom seq) and

         A9: x = (seq . k) by FUNCT_1:def 3;

        thus x in Y by A6, A8, A9;

      end;

      then

       A10: ( rng seq) c= Y;

      for n be Element of NAT holds ( inf SUPSEQ) <= (SUPSEQ . n)

      proof

        let n be Element of NAT ;

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

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

        hence thesis by XXREAL_2: 3;

      end;

      then

       A11: ( inf SUPSEQ) <= (SUPSEQ . 0 );

      now

        let x be object;

        assume x in Y;

        then

        consider k be Nat such that

         A12: x = (seq . k) & 0 <= k by A6;

        

         A13: k in NAT by ORDINAL1:def 12;

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

        hence x in ( rng seq) by A12, FUNCT_1: 3, A13;

      end;

      then Y c= ( rng seq);

      then Y = ( rng seq) by A10, XBOOLE_0:def 10;

      then (( superior_realsequence seq) . 0 ) <= p by A5, A7, XXREAL_2:def 3;

      then ( lim_sup seq) <= p by A11, XXREAL_0: 2;

      hence thesis by A1, RINFSUP2: 41;

    end;

    theorem :: MESFUNC9:10

    

     Th10: seq is convergent & (for k be Nat holds p <= (seq . k)) implies p <= ( lim seq)

    proof

      assume that

       A1: seq is convergent and

       A2: for k be Nat holds p <= (seq . k);

      for y be ExtReal holds y in ( rng seq) implies p <= y

      proof

        let y be ExtReal;

        assume y in ( rng seq);

        then

        consider x be object such that

         A3: x in ( dom seq) and

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

        reconsider x as Nat by A3;

        (seq . x) >= p by A2;

        hence thesis by A4;

      end;

      then

       A5: p is LowerBound of ( rng seq) by XXREAL_2:def 2;

      reconsider INFSEQ = ( inferior_realsequence seq) as sequence of ExtREAL ;

      consider Y be non empty Subset of ExtREAL such that

       A6: Y = { (seq . k) where k be Nat : 0 <= k } and

       A7: (INFSEQ . 0 ) = ( inf Y) by RINFSUP2:def 6;

      now

        let x be object;

        assume x in ( rng seq);

        then

        consider k be object such that

         A8: k in ( dom seq) and

         A9: x = (seq . k) by FUNCT_1:def 3;

        thus x in Y by A6, A8, A9;

      end;

      then

       A10: ( rng seq) c= Y;

      for n be Element of NAT holds ( sup INFSEQ) >= (INFSEQ . n)

      proof

        let n be Element of NAT ;

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

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

        hence thesis by XXREAL_2: 4;

      end;

      then

       A11: ( sup INFSEQ) >= (INFSEQ . 0 );

      now

        let x be object;

        assume x in Y;

        then

        consider k be Nat such that

         A12: x = (seq . k) & 0 <= k by A6;

        

         A13: k in NAT by ORDINAL1:def 12;

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

        hence x in ( rng seq) by A12, FUNCT_1: 3, A13;

      end;

      then Y c= ( rng seq);

      then Y = ( rng seq) by A10, XBOOLE_0:def 10;

      then (( inferior_realsequence seq) . 0 ) >= p by A5, A7, XXREAL_2:def 4;

      then ( lim_inf seq) >= p by A11, XXREAL_0: 2;

      hence thesis by A1, RINFSUP2: 41;

    end;

    reconsider zz = 0 as ExtReal;

    theorem :: MESFUNC9:11

    

     Th11: seq1 is convergent & seq2 is convergent & seq1 is nonnegative & seq2 is nonnegative & (for k be Nat holds (seq . k) = ((seq1 . k) + (seq2 . k))) implies seq is nonnegative & seq is convergent & ( lim seq) = (( lim seq1) + ( lim seq2))

    proof

      assume that

       A1: seq1 is convergent and

       A2: seq2 is convergent and

       A3: seq1 is nonnegative and

       A4: seq2 is nonnegative and

       A5: for k be Nat holds (seq . k) = ((seq1 . k) + (seq2 . k));

      

       A6: not seq2 is convergent_to_-infty by A4, Th8;

      for n be object st n in ( dom seq) holds 0. <= (seq . n)

      proof

        let n be object;

        assume n in ( dom seq);

        then

        reconsider n1 = n as Nat;

        

         A7: 0 <= (seq2 . n1) by A4, SUPINF_2: 51;

        

         A8: (seq . n1) = ((seq1 . n1) + (seq2 . n1)) by A5;

         0 <= (seq1 . n1) by A3, SUPINF_2: 51;

        hence thesis by A7, A8;

      end;

      hence seq is nonnegative by SUPINF_2: 52;

      

       A9: not seq1 is convergent_to_-infty by A3, Th8;

      for n be Nat holds 0 <= (seq2 . n) by A4, SUPINF_2: 51;

      then

       A10: ( lim seq2) <> -infty by A2, Th10;

      per cases by A1, A9;

        suppose

         A11: seq1 is convergent_to_+infty;

        for g be Real st 0 < g holds ex n be Nat st for m be Nat st n <= m holds g <= (seq . m)

        proof

          let g be Real;

          assume 0 < g;

          then

          consider n be Nat such that

           A12: for m be Nat st n <= m holds g <= (seq1 . m) by A11;

          take n;

          let m be Nat;

          assume n <= m;

          then

           A13: g <= (seq1 . m) by A12;

           0 <= (seq2 . m) by A4, SUPINF_2: 51;

          then (g + zz) <= ((seq1 . m) + (seq2 . m)) by A13, XXREAL_3: 36;

          then g <= ((seq1 . m) + (seq2 . m)) by XXREAL_3: 4;

          hence thesis by A5;

        end;

        then

         A14: seq is convergent_to_+infty;

        hence seq is convergent;

        then

         A15: ( lim seq) = +infty by A14, MESFUNC5:def 12;

        ( lim seq1) = +infty by A1, A11, MESFUNC5:def 12;

        hence thesis by A10, A15, XXREAL_3:def 2;

      end;

        suppose

         A16: seq1 is convergent_to_finite_number;

        then

         A17: not seq1 is convergent_to_-infty by MESFUNC5: 51;

         not seq1 is convergent_to_+infty by A16, MESFUNC5: 50;

        then

        consider g be Real such that

         A18: ( lim seq1) = g and

         A19: for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((seq1 . m) - ( lim seq1)).| < p and seq1 is convergent_to_finite_number by A1, A17, MESFUNC5:def 12;

        per cases by A2, A6;

          suppose

           A20: seq2 is convergent_to_+infty;

          for g be Real st 0 < g holds ex n be Nat st for m be Nat st n <= m holds g <= (seq . m)

          proof

            let g be Real;

            assume 0 < g;

            then

            consider n be Nat such that

             A21: for m be Nat st n <= m holds g <= (seq2 . m) by A20;

            take n;

            let m be Nat;

            assume n <= m;

            then

             A22: g <= (seq2 . m) by A21;

             0 <= (seq1 . m) by A3, SUPINF_2: 51;

            then (g + zz) <= ((seq1 . m) + (seq2 . m)) by A22, XXREAL_3: 36;

            then g <= ((seq1 . m) + (seq2 . m)) by XXREAL_3: 4;

            hence thesis by A5;

          end;

          then

           A23: seq is convergent_to_+infty;

          hence seq is convergent;

          then

           A24: ( lim seq) = +infty by A23, MESFUNC5:def 12;

          ( lim seq2) = +infty by A2, A20, MESFUNC5:def 12;

          hence thesis by A18, A24, XXREAL_3:def 2;

        end;

          suppose

           A25: seq2 is convergent_to_finite_number;

          then

           A26: not seq2 is convergent_to_-infty by MESFUNC5: 51;

           not seq2 is convergent_to_+infty by A25, MESFUNC5: 50;

          then

          consider h be Real such that

           A27: ( lim seq2) = h and

           A28: for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((seq2 . m) - ( lim seq2)).| < p and seq2 is convergent_to_finite_number by A2, A26, MESFUNC5:def 12;

          reconsider h9 = h, g9 = g as Real;

          reconsider gh = (g + h) as R_eal by XXREAL_0:def 1;

          

           A29: for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((seq . m) - (g + h)).| < p

          proof

            let p be Real;

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

            assume

             A30: 0 < p;

            then

            consider n1 be Nat such that

             A31: for m be Nat st n1 <= m holds |.((seq1 . m) - ( lim seq1)).| < (p / 2) by A19;

            consider n2 be Nat such that

             A32: for m be Nat st n2 <= m holds |.((seq2 . m) - ( lim seq2)).| < (p / 2) by A28, A30;

            reconsider n19 = n1, n29 = n2 as Element of NAT by ORDINAL1:def 12;

            reconsider n = ( max (n19,n29)) as Nat;

            take n;

            let m be Nat;

            assume

             A33: n <= m;

            

             A34: (pp / 2) in REAL by XREAL_0:def 1;

            n2 <= n by XXREAL_0: 25;

            then n2 <= m by A33, XXREAL_0: 2;

            then

             A35: |.((seq2 . m) - ( lim seq2)).| < (pp / 2) by A32;

            then |.((seq2 . m) - ( lim seq2)).| < +infty by XXREAL_0: 2, XXREAL_0: 9, A34;

            then

             A36: ((seq2 . m) - h) in REAL by A27, EXTREAL1: 41;

            n1 <= n by XXREAL_0: 25;

            then n1 <= m by A33, XXREAL_0: 2;

            then

             A37: |.((seq1 . m) - ( lim seq1)).| < (pp / 2) by A31;

            then |.((seq1 . m) - ( lim seq1)).| < +infty by XXREAL_0: 2, XXREAL_0: 9, A34;

            then ((seq1 . m) - g) in REAL by A18, EXTREAL1: 41;

            then

            consider e1,e2 be Real such that

             A38: e1 = ((seq1 . m) - g) and

             A39: e2 = ((seq2 . m) - h) by A36;

            

             A40: |.((seq2 . m) - h).| = |.e2 qua Complex.| by A39, EXTREAL1: 12;

            

             A41: 0 <= (seq2 . m) by A4, SUPINF_2: 51;

            then

             A42: ((seq2 . m) - h) <> -infty by XXREAL_3: 19;

            

             A43: 0 <= (seq1 . m) by A3, SUPINF_2: 51;

            

             A44: |.((seq1 . m) - g).| = |.e1 qua Complex.| by A38, EXTREAL1: 12;

            then

             A45: ( |.((seq2 . m) - h).| + |.((seq1 . m) - g).|) = ( |.e1 qua Complex.| + |.e2 qua Complex.|) by A40, SUPINF_2: 1;

            (g + h) = (g + h qua ExtReal);

            

            then ((seq . m) - (g + h)) = (((seq . m) - h) - g) by XXREAL_3: 31

            .= ((((seq1 . m) + (seq2 . m)) - h) - g) by A5

            .= (((seq1 . m) + ((seq2 . m) - h)) - g) by A43, A41, XXREAL_3: 30

            .= (((seq2 . m) - h) + ((seq1 . m) - g)) by A43, A42, XXREAL_3: 30;

            then

             A46: |.((seq . m) - (g + h)).| <= ( |.((seq2 . m) - h).| + |.((seq1 . m) - g).|) by EXTREAL1: 24;

            ( |.e1 qua Complex.| + |.e2 qua Complex.|) < ((p / 2) + (p / 2)) by A18, A27, A37, A35, A44, A40, XREAL_1: 8;

            hence thesis by A46, A45, XXREAL_0: 2;

          end;

          then

           A47: seq is convergent_to_finite_number;

          hence seq is convergent;

          then ( lim seq) = gh by A29, A47, MESFUNC5:def 12;

          hence thesis by A18, A27, SUPINF_2: 1;

        end;

      end;

    end;

    theorem :: MESFUNC9:12

    

     Th12: (for n be Nat holds (G . n) = ((F . n) | D)) & x in D implies ((F # x) is convergent_to_+infty implies (G # x) is convergent_to_+infty) & ((F # x) is convergent_to_-infty implies (G # x) is convergent_to_-infty) & ((F # x) is convergent_to_finite_number implies (G # x) is convergent_to_finite_number) & ((F # x) is convergent implies (G # x) is convergent)

    proof

      assume that

       A1: for n be Nat holds (G . n) = ((F . n) | D) and

       A2: x in D;

      thus

       A3: (F # x) is convergent_to_+infty implies (G # x) is convergent_to_+infty

      proof

        assume

         A4: (F # x) is convergent_to_+infty;

        let g be Real;

        assume 0 < g;

        then

        consider n be Nat such that

         A5: for m be Nat st n <= m holds g <= ((F # x) . m) by A4;

        take n;

        let m be Nat;

        assume n <= m;

        then g <= ((F # x) . m) by A5;

        then g <= ((F . m) . x) by MESFUNC5:def 13;

        then g <= (((F . m) | D) . x) by A2, FUNCT_1: 49;

        then g <= ((G . m) . x) by A1;

        hence g <= ((G # x) . m) by MESFUNC5:def 13;

      end;

      thus

       A6: (F # x) is convergent_to_-infty implies (G # x) is convergent_to_-infty

      proof

        assume

         A7: (F # x) is convergent_to_-infty;

        let g be Real;

        assume g < 0 ;

        then

        consider n be Nat such that

         A8: for m be Nat st n <= m holds ((F # x) . m) <= g by A7;

        take n;

        let m be Nat;

        assume n <= m;

        then ((F # x) . m) <= g by A8;

        then ((F . m) . x) <= g by MESFUNC5:def 13;

        then (((F . m) | D) . x) <= g by A2, FUNCT_1: 49;

        then ((G . m) . x) <= g by A1;

        hence ((G # x) . m) <= g by MESFUNC5:def 13;

      end;

      thus

       A9: (F # x) is convergent_to_finite_number implies (G # x) is convergent_to_finite_number

      proof

        assume (F # x) is convergent_to_finite_number;

        then

        consider g be Real such that

         A10: ( lim (F # x)) = g and

         A11: for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.(((F # x) . m) - ( lim (F # x))).| < p by Th7;

        for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.(((G # x) . m) - g).| < p

        proof

          let p be Real;

          assume 0 < p;

          then

          consider n be Nat such that

           A12: for m be Nat st n <= m holds |.(((F # x) . m) - ( lim (F # x))).| < p by A11;

          take n;

          let m be Nat;

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

          then ((F # x) . m) = (((F . m) | D) . x) by A2, FUNCT_1: 49;

          then

           A13: ((F # x) . m) = ((G . m) . x) by A1;

          assume n <= m;

          then |.(((F # x) . m) - ( lim (F # x))).| < p by A12;

          hence thesis by A10, A13, MESFUNC5:def 13;

        end;

        hence thesis;

      end;

      assume

       A14: (F # x) is convergent;

      per cases by A14;

        suppose (F # x) is convergent_to_+infty;

        hence thesis by A3;

      end;

        suppose (F # x) is convergent_to_-infty;

        hence thesis by A6;

      end;

        suppose (F # x) is convergent_to_finite_number;

        hence thesis by A9;

      end;

    end;

    theorem :: MESFUNC9:13

    

     Th13: E = ( dom f) & f is E -measurable & f is nonnegative & (M . (E /\ ( eq_dom (f, +infty )))) <> 0 implies ( Integral (M,f)) = +infty

    proof

      assume that

       A1: E = ( dom f) and

       A2: f is E -measurable and

       A3: f is nonnegative and

       A4: (M . (E /\ ( eq_dom (f, +infty )))) <> 0 ;

      reconsider EE = (E /\ ( eq_dom (f, +infty ))) as Element of S by A1, A2, MESFUNC1: 33;

      

       A5: ( dom (f | E)) = E by A1;

      E = (( dom f) /\ E) by A1;

      then

       A6: (f | E) is E -measurable by A2, MESFUNC5: 42;

      ( integral+ (M,(f | EE))) <= ( integral+ (M,(f | E))) by A1, A2, A3, MESFUNC5: 83, XBOOLE_1: 17;

      then

       A7: ( integral+ (M,(f | EE))) <= ( Integral (M,(f | E))) by A3, A6, A5, MESFUNC5: 15, MESFUNC5: 88;

      

       A8: EE = (( dom f) /\ EE) by A1, XBOOLE_1: 17, XBOOLE_1: 28;

      f is EE -measurable by A2, MESFUNC1: 30, XBOOLE_1: 17;

      then

       A9: (f | EE) is EE -measurable by A8, MESFUNC5: 42;

      

       A10: (f | EE) is nonnegative by A3, MESFUNC5: 15;

      reconsider ES = {} as Element of S by PROB_1: 4;

      deffunc G( Element of NAT ) = ($1 (#) (( chi (EE,X)) | EE));

      consider G be Function such that

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

      now

        let g be object;

        assume g in ( rng G);

        then

        consider m be object such that

         A12: m in ( dom G) and

         A13: g = (G . m) by FUNCT_1:def 3;

        reconsider m as Element of NAT by A11, A12;

        g = (m (#) (( chi (EE,X)) | EE)) by A11, A13;

        hence g in ( PFuncs (X, ExtREAL )) by PARTFUN1: 45;

      end;

      then ( rng G) c= ( PFuncs (X, ExtREAL ));

      then

      reconsider G as Functional_Sequence of X, ExtREAL by A11, FUNCT_2:def 1, RELSET_1: 4;

      

       A14: for n be Nat holds ( dom (G . n)) = EE & for x be set st x in ( dom (G . n)) holds ((G . n) . x) = n

      proof

        let n be Nat;

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

        EE c= X;

        then EE c= ( dom ( chi (EE,X))) by FUNCT_3:def 3;

        then

         A15: ( dom (( chi (EE,X)) | EE)) = EE by RELAT_1: 62;

        

         A16: (G . n) = (n1 (#) (( chi (EE,X)) | EE)) by A11;

        hence

         A17: ( dom (G . n)) = EE by A15, MESFUNC1:def 6;

        let x be set;

        assume

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

        then

        reconsider x1 = x as Element of X;

        (( chi (EE,X)) . x1) = 1. by A17, A18, FUNCT_3:def 3;

        then ((( chi (EE,X)) | EE) . x1) = 1. by A15, A17, A18, FUNCT_1: 47;

        then ((G . n) . x) = (n1 * 1. ) by A16, A18, MESFUNC1:def 6;

        hence thesis by XXREAL_3: 81;

      end;

      

       A19: for n be Nat holds (G . n) is nonnegative

      proof

        let n be Nat;

        for x be object st x in ( dom (G . n)) holds 0 <= ((G . n) . x) by A14;

        hence thesis by SUPINF_2: 52;

      end;

      deffunc K( Element of NAT ) = ( integral' (M,(G . $1)));

      consider K be sequence of ExtREAL such that

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

      reconsider K as ExtREAL_sequence;

      

       A21: for n be Nat holds (K . n) = ( integral' (M,(G . n)))

      proof

        let n be Nat;

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

        (K . n) = ( integral' (M,(G . n1))) by A20;

        hence thesis;

      end;

      

       A22: ( dom (f | EE)) = EE by A1, RELAT_1: 62, XBOOLE_1: 17;

      

       A23: for n,m be Nat st n <= m holds for x be Element of X st x in ( dom (f | EE)) holds ((G . n) . x) <= ((G . m) . x)

      proof

        let n,m be Nat such that

         A24: n <= m;

        let x be Element of X;

        assume

         A25: x in ( dom (f | EE));

        then x in ( dom (G . n)) by A22, A14;

        then

         A26: ((G . n) . x) = n by A14;

        x in ( dom (G . m)) by A22, A14, A25;

        hence thesis by A14, A24, A26;

      end;

      

       A27: for n be Nat holds ( dom (G . n)) = ( dom (f | EE)) & (G . n) is_simple_func_in S

      proof

        let n be Nat;

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

        thus

         A28: ( dom (G . n)) = ( dom (f | EE)) by A22, A14;

        for x be object st x in ( dom (G . n)) holds ((G . n) . x) = n1 by A14;

        hence thesis by A22, A28, MESFUNC6: 2;

      end;

      

       A29: for i be Element of NAT holds (K . i) = (i * (M . ( dom (G . i))))

      proof

        let i be Element of NAT ;

        reconsider ii = i as R_eal by XXREAL_0:def 1;

        for x be object st x in ( dom (G . i)) holds ((G . ii) . x) = ii by A14;

        then ( integral' (M,(G . i))) = (ii * (M . ( dom (G . ii)))) by A27, MESFUNC5: 71;

        hence thesis by A21;

      end;

      (M . ES) <= (M . EE) by MEASURE1: 31, XBOOLE_1: 2;

      then

       A30: ( In ( 0 , REAL )) < (M . EE) by A4, VALUED_0:def 19;

      

       A31: not ( rng K) is bounded_above

      proof

        assume ( rng K) is bounded_above;

        then

        consider UB be Real such that

         A32: UB is UpperBound of ( rng K) by XXREAL_2:def 10;

        reconsider r = UB as Real;

        per cases by A30, XXREAL_0: 10;

          suppose

           A33: (M . EE) = +infty ;

          (K . 1) = (1 * (M . ( dom (G . 1)))) by A29;

          then (K . 1) = (1 * (M . EE)) by A14;

          then

           A34: (K . 1) = +infty by A33, XXREAL_3:def 5;

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

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

          then (K . 1) <= UB by A32, XXREAL_2:def 1;

          hence contradiction by A34, XXREAL_0: 4;

        end;

          suppose (M . EE) in REAL ;

          then

          reconsider ee = (M . EE) as Real;

          consider n be Nat such that

           A35: (r / ee) < n by SEQ_4: 3;

          

           A36: n in NAT by ORDINAL1:def 12;

          (K . n) = (n * (M . ( dom (G . n)))) by A29, A36;

          then (K . n) = (n * (M . EE)) by A14;

          then

           A37: (K . n) = (n * ee) by EXTREAL1: 1;

          ((r / ee) * ee) < (n * ee) by A30, A35, XREAL_1: 68;

          then (r / (ee / ee)) < (K . n) by A37, XCMPLX_1: 82;

          then

           A38: r < (K . n) by A4, XCMPLX_1: 51;

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

          then (K . n) in ( rng K) by FUNCT_1: 3, A36;

          then (K . n) <= r by A32, XXREAL_2:def 1;

          hence contradiction by A38;

        end;

      end;

      for n,m be Nat st m <= n holds (K . m) <= (K . n)

      proof

        let n,m be Nat;

        

         A39: n in NAT by ORDINAL1:def 12;

        

         A40: m in NAT by ORDINAL1:def 12;

        ( dom (G . m)) = EE by A14;

        then

         A41: (K . m) = (m * (M . EE)) by A29, A40;

        ( dom (G . n)) = EE by A14;

        then

         A42: (K . n) = (n * (M . EE)) by A29, A39;

        assume m <= n;

        hence thesis by A30, A41, A42, XXREAL_3: 71;

      end;

      then

       A43: K is non-decreasing by RINFSUP2: 7;

      then

       A44: ( lim K) = ( sup K) by RINFSUP2: 37;

      

       A45: for x be Element of X st x in ( dom (f | EE)) holds (G # x) is convergent & ( lim (G # x)) = ((f | EE) . x)

      proof

        let x be Element of X;

        assume

         A46: x in ( dom (f | EE));

        then

         A47: x in EE by A1, RELAT_1: 62, XBOOLE_1: 17;

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

        then (f . x) = +infty by MESFUNC1:def 15;

        then

         A48: ((f | EE) . x) = +infty by A47, FUNCT_1: 49;

        

         A49: not ( rng (G # x)) is bounded_above

        proof

          assume ( rng (G # x)) is bounded_above;

          then

          consider UB be Real such that

           A50: UB is UpperBound of ( rng (G # x)) by XXREAL_2:def 10;

          reconsider r = UB as Real;

          consider n be Nat such that

           A51: r < n by SEQ_4: 3;

          x in ( dom (G . n)) by A14, A47;

          then ((G . n) . x) = n by A14;

          then

           A52: UB < ((G # x) . n) by A51, MESFUNC5:def 13;

          

           A53: n in NAT by ORDINAL1:def 12;

          ( dom (G # x)) = NAT by FUNCT_2:def 1;

          then ((G # x) . n) in ( rng (G # x)) by FUNCT_1: 3, A53;

          hence contradiction by A52, A50, XXREAL_2:def 1;

        end;

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

        proof

          let n,m be Nat;

          ( dom (G . n)) = EE by A14;

          then

           A54: ((G . n) . x) = n by A22, A14, A46;

          ( dom (G . m)) = EE by A14;

          then ((G . m) . x) = m by A22, A14, A46;

          then

           A55: ((G # x) . m) = m by MESFUNC5:def 13;

          assume m <= n;

          hence thesis by A54, A55, MESFUNC5:def 13;

        end;

        then

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

        ( sup ( rng (G # x))) is UpperBound of ( rng (G # x)) by XXREAL_2:def 3;

        then ( sup (G # x)) = +infty by A49, XXREAL_2: 53;

        hence thesis by A56, A48, RINFSUP2: 37;

      end;

      ( sup ( rng K)) is UpperBound of ( rng K) by XXREAL_2:def 3;

      then

       A57: ( sup K) = +infty by A31, XXREAL_2: 53;

      K is convergent by A43, RINFSUP2: 37;

      then ( integral+ (M,(f | EE))) = +infty by A10, A22, A9, A27, A19, A23, A45, A21, A44, A57, MESFUNC5:def 15;

      then ( Integral (M,(f | E))) = +infty by A7, XXREAL_0: 4;

      hence thesis by A1;

    end;

    reconsider jj = 1 as Real;

    theorem :: MESFUNC9:14

    ( Integral (M,( chi (E,X)))) = (M . E) & ( Integral (M,(( chi (E,X)) | E))) = (M . E)

    proof

      reconsider XX = X as Element of S by MEASURE1: 7;

      set F = (XX \ E);

       A1:

      now

        let x be Element of X;

        assume

         A2: x in ( dom ( max- ( chi (E,X))));

        per cases ;

          suppose x in E;

          then (( chi (E,X)) . x) = 1 by FUNCT_3:def 3;

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

          hence (( max- ( chi (E,X))) . x) = 0 by A2, MESFUNC2:def 3;

        end;

          suppose not x in E;

          then (( chi (E,X)) . x) = 0. by FUNCT_3:def 3;

          then ( - (( chi (E,X)) . x)) = 0 ;

          then ( max (( - (( chi (E,X)) . x)), 0. )) = 0 ;

          hence (( max- ( chi (E,X))) . x) = 0 by A2, MESFUNC2:def 3;

        end;

      end;

      

       A3: XX = ( dom ( chi (E,X))) by FUNCT_3:def 3;

      then

       A4: XX = ( dom ( max+ ( chi (E,X)))) by MESFUNC7: 23;

      

       A5: (XX /\ F) = F by XBOOLE_1: 28;

      then

       A6: ( dom (( max+ ( chi (E,X))) | F)) = F by A4, RELAT_1: 61;

       A7:

      now

        let x be Element of X;

        assume

         A8: x in ( dom (( max+ ( chi (E,X))) | F));

        then (( chi (E,X)) . x) = 0 by A6, FUNCT_3: 37;

        then (( max+ ( chi (E,X))) . x) = 0 by MESFUNC7: 23;

        hence ((( max+ ( chi (E,X))) | F) . x) = 0 by A8, FUNCT_1: 47;

      end;

      

       A9: ( chi (E,X)) is XX -measurable by MESFUNC2: 29;

      then

       A10: ( max+ ( chi (E,X))) is XX -measurable by MESFUNC7: 23;

      then ( max+ ( chi (E,X))) is F -measurable by MESFUNC1: 30;

      then

       A11: ( integral+ (M,(( max+ ( chi (E,X))) | F))) = 0 by A4, A5, A6, A7, MESFUNC5: 42, MESFUNC5: 87;

      

       A12: (XX /\ E) = E by XBOOLE_1: 28;

      then

       A13: ( dom (( max+ ( chi (E,X))) | E)) = E by A4, RELAT_1: 61;

      (E \/ F) = XX by A12, XBOOLE_1: 51;

      then

       A14: (( max+ ( chi (E,X))) | (E \/ F)) = ( max+ ( chi (E,X)));

      

       A15: for x be object st x in ( dom ( max+ ( chi (E,X)))) holds 0. <= (( max+ ( chi (E,X))) . x) by MESFUNC2: 12;

      then

       A16: ( max+ ( chi (E,X))) is nonnegative by SUPINF_2: 52;

      then ( integral+ (M,(( max+ ( chi (E,X))) | (E \/ F)))) = (( integral+ (M,(( max+ ( chi (E,X))) | E))) + ( integral+ (M,(( max+ ( chi (E,X))) | F)))) by A4, A10, MESFUNC5: 81, XBOOLE_1: 79;

      then

       A17: ( integral+ (M,( max+ ( chi (E,X))))) = ( integral+ (M,(( max+ ( chi (E,X))) | E))) by A14, A11, XXREAL_3: 4;

       A18:

      now

        let x be object;

        assume

         A19: x in ( dom (( max+ ( chi (E,X))) | E));

        then (( chi (E,X)) . x) = 1 by A13, FUNCT_3:def 3;

        then (( max+ ( chi (E,X))) . x) = 1 by MESFUNC7: 23;

        hence ((( max+ ( chi (E,X))) | E) . x) = 1 by A19, FUNCT_1: 47;

      end;

      then (( max+ ( chi (E,X))) | E) is_simple_func_in S by A13, MESFUNC6: 2;

      then ( integral+ (M,( max+ ( chi (E,X))))) = ( integral' (M,(( max+ ( chi (E,X))) | E))) by A16, A17, MESFUNC5: 15, MESFUNC5: 77;

      then

       A20: ( integral+ (M,( max+ ( chi (E,X))))) = (jj * (M . ( dom (( max+ ( chi (E,X))) | E)))) by A13, A18, MESFUNC5: 104;

      ( max+ ( chi (E,X))) is E -measurable by A10, MESFUNC1: 30;

      then (( max+ ( chi (E,X))) | E) is E -measurable by A4, A12, MESFUNC5: 42;

      then

       A21: (( chi (E,X)) | E) is E -measurable by MESFUNC7: 23;

      (( max+ ( chi (E,X))) | E) is nonnegative by A15, MESFUNC5: 15, SUPINF_2: 52;

      then

       A22: (( chi (E,X)) | E) is nonnegative by MESFUNC7: 23;

      E = ( dom (( chi (E,X)) | E)) by A13, MESFUNC7: 23;

      then

       A23: ( Integral (M,(( chi (E,X)) | E))) = ( integral+ (M,(( chi (E,X)) | E))) by A21, A22, MESFUNC5: 88;

      XX = ( dom ( max- ( chi (E,X)))) by A3, MESFUNC2:def 3;

      then ( integral+ (M,( max- ( chi (E,X))))) = 0 by A3, A9, A1, MESFUNC2: 26, MESFUNC5: 87;

      then ( Integral (M,( chi (E,X)))) = (1 * (M . E)) by A13, A20, XXREAL_3: 15;

      hence ( Integral (M,( chi (E,X)))) = (M . E) by XXREAL_3: 81;

      (( chi (E,X)) | E) = (( max+ ( chi (E,X))) | E) by MESFUNC7: 23;

      hence thesis by A13, A17, A20, A23, XXREAL_3: 81;

    end;

    theorem :: MESFUNC9:15

    

     Th15: E c= ( dom f) & E c= ( dom g) & f is E -measurable & g is E -measurable & f is nonnegative & (for x be Element of X st x in E holds (f . x) <= (g . x)) implies ( Integral (M,(f | E))) <= ( Integral (M,(g | E)))

    proof

      assume that

       A1: E c= ( dom f) and

       A2: E c= ( dom g) and

       A3: f is E -measurable and

       A4: g is E -measurable and

       A5: f is nonnegative and

       A6: for x be Element of X st x in E holds (f . x) <= (g . x);

      set F2 = (g | E);

      

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

      set F1 = (f | E);

      

       A8: F1 is nonnegative by A5, MESFUNC5: 15;

      

       A9: E = ( dom (g | E)) by A2, RELAT_1: 62;

      

       A10: for x be Element of X st x in ( dom F1) holds (F1 . x) <= (F2 . x)

      proof

        let x be Element of X;

        assume

         A11: x in ( dom F1);

        then

         A12: (F1 . x) = (f . x) by FUNCT_1: 47;

        (F2 . x) = (g . x) by A7, A9, A11, FUNCT_1: 47;

        hence thesis by A6, A7, A11, A12;

      end;

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

      proof

        let x be object;

        assume

         A13: x in ( dom F2);

         0 <= (F1 . x) by A8, SUPINF_2: 51;

        hence thesis by A7, A9, A10, A13;

      end;

      then

       A14: F2 is nonnegative by SUPINF_2: 52;

      

       A15: (( dom g) /\ E) = E by A2, XBOOLE_1: 28;

      then

       A16: F2 is E -measurable by A4, MESFUNC5: 42;

      

       A17: (( dom f) /\ E) = E by A1, XBOOLE_1: 28;

      then F1 is E -measurable by A3, MESFUNC5: 42;

      then ( integral+ (M,F1)) <= ( integral+ (M,F2)) by A8, A7, A9, A10, A14, A16, MESFUNC5: 85;

      then ( Integral (M,F1)) <= ( integral+ (M,F2)) by A3, A8, A7, A17, MESFUNC5: 42, MESFUNC5: 88;

      hence thesis by A4, A9, A14, A15, MESFUNC5: 42, MESFUNC5: 88;

    end;

    begin

    definition

      let s be ext-real-valued Function;

      :: MESFUNC9:def1

      func Partial_Sums s -> ExtREAL_sequence means

      : Def1: (it . 0 ) = (s . 0 ) & for n be Nat holds (it . (n + 1)) = ((it . n) + (s . (n + 1)));

      existence

      proof

        deffunc U( Nat, R_eal) = ($2 + (s . ($1 + 1)));

        consider f be sequence of ExtREAL such that

         A1: (f . 0 ) = (s . 0 ) & for n be Nat holds (f . (n + 1)) = U(n,.) from NAT_1:sch 12;

        take f;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let s1,s2 be ExtREAL_sequence;

        assume that

         A2: (s1 . 0 ) = (s . 0 ) and

         A3: for n be Nat holds (s1 . (n + 1)) = ((s1 . n) + (s . (n + 1))) and

         A4: (s2 . 0 ) = (s . 0 ) and

         A5: for n be Nat holds (s2 . (n + 1)) = ((s2 . n) + (s . (n + 1)));

        defpred X[ Nat] means (s1 . $1) = (s2 . $1);

        

         A6: for k be Nat st X[k] holds X[(k + 1)]

        proof

          let k be Nat;

          assume (s1 . k) = (s2 . k);

          

          hence (s1 . (k + 1)) = ((s2 . k) + (s . (k + 1))) by A3

          .= (s2 . (k + 1)) by A5;

        end;

        

         A7: X[ 0 ] by A2, A4;

        for n be Nat holds X[n] from NAT_1:sch 2( A7, A6);

        hence s1 = s2;

      end;

    end

    definition

      let s be ext-real-valued Function;

      :: MESFUNC9:def2

      attr s is summable means ( Partial_Sums s) is convergent;

    end

    definition

      let s be ext-real-valued Function;

      :: MESFUNC9:def3

      func Sum s -> R_eal equals ( lim ( Partial_Sums s));

      correctness ;

    end

    theorem :: MESFUNC9:16

    

     Th16: seq is nonnegative implies ( Partial_Sums seq) is nonnegative & ( Partial_Sums seq) is non-decreasing

    proof

      set PS = ( Partial_Sums seq);

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

      assume

       A1: seq is nonnegative;

      

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

      proof

        let k be Nat;

        assume

         A3: P[k];

        

         A4: (PS . (k + 1)) = ((PS . k) + (seq . (k + 1))) by Def1;

        (seq . (k + 1)) >= 0 by A1, SUPINF_2: 51;

        hence thesis by A3, A4;

      end;

      (PS . 0 ) = (seq . 0 ) by Def1;

      then

       A5: P[ 0 ] by A1, SUPINF_2: 51;

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

      then for k be object st k in ( dom PS) holds 0 <= (PS . k);

      hence PS is nonnegative by SUPINF_2: 52;

      for n,m be Nat st m <= n holds (( Partial_Sums seq) . m) <= (( Partial_Sums seq) . n)

      proof

        let n,m be Nat;

        reconsider m1 = m as Nat;

        defpred Q[ Nat] means (PS . m1) <= (PS . $1);

        

         A6: for k be Nat holds (PS . k) <= (PS . (k + 1))

        proof

          let k be Nat;

          

           A7: 0 <= (seq . (k + 1)) by A1, SUPINF_2: 51;

          (PS . (k + 1)) = ((PS . k) + (seq . (k + 1))) by Def1;

          hence thesis by A7, XXREAL_3: 39;

        end;

        

         A8: for k be Nat st k >= m1 & (for l be Nat st l >= m1 & l < k holds Q[l]) holds Q[k]

        proof

          let k be Nat;

          assume that

           A9: k >= m1 and

           A10: for l be Nat st l >= m1 & l < k holds Q[l];

          now

            assume k > m1;

            then

             A11: k >= (m1 + 1) by NAT_1: 13;

            per cases by A11, XXREAL_0: 1;

              suppose k = (m1 + 1);

              hence thesis by A6;

            end;

              suppose

               A12: k > (m1 + 1);

              then

              reconsider l = (k - 1) as Element of NAT by NAT_1: 20;

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

              then

               A13: k > l by XREAL_1: 19;

              k = (l + 1);

              then

               A14: (PS . l) <= (PS . k) by A6;

              l >= m1 by A12, XREAL_1: 19;

              then (PS . m1) <= (PS . l) by A10, A13;

              hence thesis by A14, XXREAL_0: 2;

            end;

          end;

          hence thesis by A9, XXREAL_0: 1;

        end;

        

         A15: for k be Nat st k >= m1 holds Q[k] from NAT_1:sch 9( A8);

        assume m <= n;

        hence thesis by A15;

      end;

      hence thesis by RINFSUP2: 7;

    end;

    theorem :: MESFUNC9:17

    (for n be Nat holds 0 < (seq . n)) implies for m be Nat holds 0 < (( Partial_Sums seq) . m)

    proof

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

      assume

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

      

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

      proof

        let k be Nat;

        assume

         A3: P[k];

        

         A4: (( Partial_Sums seq) . (k + 1)) = ((( Partial_Sums seq) . k) + (seq . (k + 1))) by Def1;

        (seq . (k + 1)) > 0 by A1;

        hence thesis by A3, A4;

      end;

      (( Partial_Sums seq) . 0 ) = (seq . 0 ) by Def1;

      then

       A5: P[ 0 ] by A1;

      thus for m be Nat holds P[m] from NAT_1:sch 2( A5, A2);

    end;

    theorem :: MESFUNC9:18

    

     Th18: F is with_the_same_dom & (for n be Nat holds (G . n) = ((F . n) | D)) implies G is with_the_same_dom

    proof

      assume that

       A1: F is with_the_same_dom and

       A2: for n be Nat holds (G . n) = ((F . n) | D);

      let n,m be Nat;

      (G . m) = ((F . m) | D) by A2;

      then

       A3: ( dom (G . m)) = (( dom (F . m)) /\ D) by RELAT_1: 61;

      (G . n) = ((F . n) | D) by A2;

      then ( dom (G . n)) = (( dom (F . n)) /\ D) by RELAT_1: 61;

      hence thesis by A1, A3;

    end;

    theorem :: MESFUNC9:19

    

     Th19: D c= ( dom (F . 0 )) & (for n be Nat holds (G . n) = ((F . n) | D)) & (for x be Element of X st x in D holds (F # x) is convergent) implies (( lim F) | D) = ( lim G)

    proof

      assume that

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

       A2: for n be Nat holds (G . n) = ((F . n) | D) and

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

      (G . 0 ) = ((F . 0 ) | D) by A2;

      then

       A4: ( dom (G . 0 )) = D by A1, RELAT_1: 62;

      

       A5: ( dom (( lim F) | D)) = (( dom ( lim F)) /\ D) by RELAT_1: 61;

      then ( dom (( lim F) | D)) = (( dom (F . 0 )) /\ D) by MESFUNC8:def 9;

      then ( dom (( lim F) | D)) = D by A1, XBOOLE_1: 28;

      then

       A6: ( dom (( lim F) | D)) = ( dom ( lim G)) by A4, MESFUNC8:def 9;

      now

        let x be Element of X;

        assume

         A7: x in ( dom (( lim F) | D));

        then

         A8: ((( lim F) | D) . x) = (( lim F) . x) by FUNCT_1: 47;

        x in ( dom ( lim F)) by A5, A7, XBOOLE_0:def 4;

        then

         A9: ((( lim F) | D) . x) = ( lim (F # x)) by A8, MESFUNC8:def 9;

        

         A10: x in D by A7, RELAT_1: 57;

        then

         A11: (F # x) is convergent by A3;

        per cases by A11;

          suppose

           A12: (F # x) is convergent_to_+infty;

          then (G # x) is convergent_to_+infty by A2, A10, Th12;

          then ( lim (G # x)) = +infty by Th7;

          then (( lim G) . x) = +infty by A6, A7, MESFUNC8:def 9;

          hence (( lim G) . x) = ((( lim F) | D) . x) by A9, A12, Th7;

        end;

          suppose

           A13: (F # x) is convergent_to_-infty;

          then (G # x) is convergent_to_-infty by A2, A10, Th12;

          then ( lim (G # x)) = -infty by Th7;

          then (( lim G) . x) = -infty by A6, A7, MESFUNC8:def 9;

          hence (( lim G) . x) = ((( lim F) | D) . x) by A9, A13, Th7;

        end;

          suppose

           A14: (F # x) is convergent_to_finite_number;

          then

          consider g be Real such that

           A15: ( lim (F # x)) = g and

           A16: for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.(((F # x) . m) - ( lim (F # x))).| < p by Th7;

           A17:

          now

            let p be Real;

            assume 0 < p;

            then

            consider n be Nat such that

             A18: for m be Nat st n <= m holds |.(((F # x) . m) - ( lim (F # x))).| < p by A16;

            take n;

            let m be Nat;

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

            then ((F # x) . m) = (((F . m) | D) . x) by A10, FUNCT_1: 49;

            then

             A19: ((F # x) . m) = ((G . m) . x) by A2;

            assume n <= m;

            then |.(((F # x) . m) - ( lim (F # x))).| < p by A18;

            hence |.(((G # x) . m) - g).| < p by A15, A19, MESFUNC5:def 13;

          end;

          reconsider g as R_eal by XXREAL_0:def 1;

          

           A20: (G # x) is convergent_to_finite_number by A2, A10, A14, Th12;

          then (G # x) is convergent;

          then ( lim (G # x)) = g by A17, A20, MESFUNC5:def 12;

          hence (( lim G) . x) = ((( lim F) | D) . x) by A6, A7, A9, A15, MESFUNC8:def 9;

        end;

      end;

      hence thesis by A6, PARTFUN1: 5;

    end;

    theorem :: MESFUNC9:20

    

     Th20: F is with_the_same_dom & E c= ( dom (F . 0 )) & (for m be Nat holds (F . m) is E -measurable & (G . m) = ((F . m) | E)) implies (G . n) is E -measurable

    proof

      assume that

       A1: F is with_the_same_dom and

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

       A3: for m be Nat holds (F . m) is E -measurable & (G . m) = ((F . m) | E);

      ( dom (F . n)) = ( dom (F . 0 )) by A1;

      then (( dom (F . n)) /\ E) = E by A2, XBOOLE_1: 28;

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

      hence thesis by A3;

    end;

    theorem :: MESFUNC9:21

    

     Th21: E c= ( dom (F . 0 )) & G is with_the_same_dom & (for x be Element of X st x in E holds (F # x) is summable) & (for n be Nat holds (G . n) = ((F . n) | E)) implies for x be Element of X st x in E holds (G # x) is summable

    proof

      assume that

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

       A2: G is with_the_same_dom and

       A3: for x be Element of X st x in E holds (F # x) is summable and

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

      let x be Element of X;

      assume

       A5: x in E;

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

      then

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

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

      proof

        let n be Element of NAT ;

        ( dom (G . n)) = E by A2, A6;

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

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

        then

         A7: ((G . n) . x) = ((F . n) . x) by A4;

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

        hence thesis by A7, MESFUNC5:def 13;

      end;

      then

       A8: ( Partial_Sums (F # x)) = ( Partial_Sums (G # x)) by FUNCT_2: 63;

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

      then ( Partial_Sums (F # x)) is convergent;

      hence thesis by A8;

    end;

    begin

    definition

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

      :: MESFUNC9:def4

      func Partial_Sums F -> Functional_Sequence of X, ExtREAL means

      : Def4: (it . 0 ) = (F . 0 ) & for n be Nat holds (it . (n + 1)) = ((it . n) + (F . (n + 1)));

      existence

      proof

        defpred P[ Nat, set, set] means ( not $2 is PartFunc of X, ExtREAL & $3 = (F . $1)) or ($2 is PartFunc of X, ExtREAL & for F2 be PartFunc of X, ExtREAL st F2 = $2 holds $3 = (F2 + (F . ($1 + 1))));

        

         A1: for n be Nat holds for x be set holds ex y be set st P[n, x, y]

        proof

          let n be Nat;

          let x be set;

          thus ex y be set st P[n, x, y]

          proof

            per cases ;

              suppose

               A2: not x is PartFunc of X, ExtREAL ;

              take y = (F . n);

              thus not x is PartFunc of X, ExtREAL & y = (F . n) or (x is PartFunc of X, ExtREAL & for F2 be PartFunc of X, ExtREAL st F2 = x holds y = (F2 + (F . (n + 1)))) by A2;

            end;

              suppose x is PartFunc of X, ExtREAL ;

              then

              reconsider G2 = x as PartFunc of X, ExtREAL ;

              take y = (G2 + (F . (n + 1)));

              thus not x is PartFunc of X, ExtREAL & y = (F . n) or (x is PartFunc of X, ExtREAL & for F2 be PartFunc of X, ExtREAL st F2 = x holds y = (F2 + (F . (n + 1))));

            end;

          end;

        end;

        consider IT be Function such that

         A3: ( dom IT) = NAT & (IT . 0 ) = (F . 0 ) & for n be Nat holds P[n, (IT . n), (IT . (n + 1))] from RECDEF_1:sch 1( A1);

        now

          defpred IND[ Nat] means (IT . $1) is PartFunc of X, ExtREAL ;

          let f be object;

          assume f in ( rng IT);

          then

          consider m be object such that

           A4: m in ( dom IT) and

           A5: f = (IT . m) by FUNCT_1:def 3;

          reconsider m as Element of NAT by A3, A4;

          

           A6: for n be Nat st IND[n] holds IND[(n + 1)]

          proof

            let n be Nat;

            assume IND[n];

            then

            reconsider F2 = (IT . n) as PartFunc of X, ExtREAL ;

            (IT . (n + 1)) = (F2 + (F . (n + 1))) by A3;

            hence thesis;

          end;

          

           A7: IND[ 0 ] by A3;

          for n be Nat holds IND[n] from NAT_1:sch 2( A7, A6);

          then (IT . m) is PartFunc of X, ExtREAL ;

          hence f in ( PFuncs (X, ExtREAL )) by A5, PARTFUN1: 45;

        end;

        then ( rng IT) c= ( PFuncs (X, ExtREAL ));

        then

        reconsider IT as Functional_Sequence of X, ExtREAL by A3, FUNCT_2:def 1, RELSET_1: 4;

        take IT;

        thus thesis by A3;

      end;

      uniqueness

      proof

        let PS1,PS2 be Functional_Sequence of X, ExtREAL ;

        assume that

         A8: (PS1 . 0 ) = (F . 0 ) and

         A9: for n be Nat holds (PS1 . (n + 1)) = ((PS1 . n) + (F . (n + 1))) and

         A10: (PS2 . 0 ) = (F . 0 ) and

         A11: for n be Nat holds (PS2 . (n + 1)) = ((PS2 . n) + (F . (n + 1)));

        defpred IND[ Nat] means (PS1 . $1) = (PS2 . $1);

        

         A12: for n be Nat st IND[n] holds IND[(n + 1)]

        proof

          let n be Nat;

          assume

           A13: IND[n];

          (PS1 . (n + 1)) = ((PS1 . n) + (F . (n + 1))) by A9;

          hence thesis by A11, A13;

        end;

        

         A14: IND[ 0 ] by A8, A10;

        for n be Nat holds IND[n] from NAT_1:sch 2( A14, A12);

        then for m be Element of NAT holds (PS1 . m) = (PS2 . m);

        hence thesis;

      end;

    end

    definition

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

      :: MESFUNC9:def5

      attr F is additive means for n,m be Nat st n <> m holds for x be set st x in (( dom (F . n)) /\ ( dom (F . m))) holds ((F . n) . x) <> +infty or ((F . m) . x) <> -infty ;

    end

    

     Lm1: z in ( dom (( Partial_Sums F) . n)) & m <= n implies z in ( dom (( Partial_Sums F) . m))

    proof

      set PF = ( Partial_Sums F);

      assume that

       A1: z in ( dom (PF . n)) and

       A2: m <= n;

      defpred P[ Nat] means m <= $1 & $1 <= n implies not z in ( dom (PF . $1));

      assume

       A3: not z in ( dom (PF . m));

      

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

      proof

        let k be Nat;

        assume

         A5: P[k];

        assume that

         A6: m <= (k + 1) and

         A7: (k + 1) <= n;

        per cases by A6, NAT_1: 8;

          suppose

           A8: m <= k;

          (PF . (k + 1)) = ((PF . k) + (F . (k + 1))) by Def4;

          then

           A9: ( dom (PF . (k + 1))) = ((( dom (PF . k)) /\ ( dom (F . (k + 1)))) \ ((((PF . k) " { -infty }) /\ ((F . (k + 1)) " { +infty })) \/ (((PF . k) " { +infty }) /\ ((F . (k + 1)) " { -infty })))) by MESFUNC1:def 3;

           not z in (( dom (PF . k)) /\ ( dom (F . (k + 1)))) by A5, A7, A8, NAT_1: 13, XBOOLE_0:def 4;

          hence thesis by A9, XBOOLE_0:def 5;

        end;

          suppose m = (k + 1);

          hence thesis by A3;

        end;

      end;

      

       A10: P[ 0 ] by A3;

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

      hence contradiction by A1, A2;

    end;

    theorem :: MESFUNC9:22

    

     Th22: z in ( dom (( Partial_Sums F) . n)) & m <= n implies z in ( dom (( Partial_Sums F) . m)) & z in ( dom (F . m))

    proof

      set PF = ( Partial_Sums F);

      assume that

       A1: z in ( dom (PF . n)) and

       A2: m <= n;

      thus

       A3: z in ( dom (PF . m)) by A1, A2, Lm1;

      per cases ;

        suppose m = 0 ;

        then (PF . m) = (F . m) by Def4;

        hence thesis by A1, A2, Lm1;

      end;

        suppose m <> 0 ;

        then

        consider k be Nat such that

         A4: m = (k + 1) by NAT_1: 6;

        (PF . m) = ((PF . k) + (F . m)) by A4, Def4;

        then ( dom (PF . m)) = ((( dom (PF . k)) /\ ( dom (F . m))) \ ((((PF . k) " { -infty }) /\ ((F . m) " { +infty })) \/ (((PF . k) " { +infty }) /\ ((F . m) " { -infty })))) by MESFUNC1:def 3;

        then z in (( dom (PF . k)) /\ ( dom (F . m))) by A3, XBOOLE_0:def 5;

        hence thesis by XBOOLE_0:def 4;

      end;

    end;

    theorem :: MESFUNC9:23

    

     Th23: z in ( dom (( Partial_Sums F) . n)) & ((( Partial_Sums F) . n) . z) = +infty implies ex m be Nat st m <= n & ((F . m) . z) = +infty

    proof

      set PF = ( Partial_Sums F);

      assume that

       A1: z in ( dom (PF . n)) and

       A2: ((PF . n) . z) = +infty ;

      now

        defpred P[ Nat] means $1 <= n implies ((PF . $1) . z) <> +infty ;

        assume

         A3: for m be Element of NAT st m <= n holds ((F . m) . z) <> +infty ;

        

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

        proof

          let k be Nat;

          assume

           A5: P[k];

          assume

           A6: (k + 1) <= n;

          then k <= n by NAT_1: 13;

          then

           A7: z in ( dom (PF . k)) by A1, Th22;

           not ((PF . k) . z) in { +infty } by A5, A6, NAT_1: 13, TARSKI:def 1;

          then not z in ((PF . k) " { +infty }) by FUNCT_1:def 7;

          then

           A8: not z in (((PF . k) " { +infty }) /\ ((F . (k + 1)) " { -infty })) by XBOOLE_0:def 4;

          z in ( dom (F . (k + 1))) by A1, A6, Th22;

          then

           A9: z in (( dom (PF . k)) /\ ( dom (F . (k + 1)))) by A7, XBOOLE_0:def 4;

          

           A10: (PF . (k + 1)) = ((PF . k) + (F . (k + 1))) by Def4;

          

           A11: ((F . (k + 1)) . z) <> +infty by A3, A6;

          then not ((F . (k + 1)) . z) in { +infty } by TARSKI:def 1;

          then not z in ((F . (k + 1)) " { +infty }) by FUNCT_1:def 7;

          then not z in (((PF . k) " { -infty }) /\ ((F . (k + 1)) " { +infty })) by XBOOLE_0:def 4;

          then not z in ((((PF . k) " { +infty }) /\ ((F . (k + 1)) " { -infty })) \/ (((PF . k) " { -infty }) /\ ((F . (k + 1)) " { +infty }))) by A8, XBOOLE_0:def 3;

          then z in ((( dom (PF . k)) /\ ( dom (F . (k + 1)))) \ ((((PF . k) " { +infty }) /\ ((F . (k + 1)) " { -infty })) \/ (((PF . k) " { -infty }) /\ ((F . (k + 1)) " { +infty })))) by A9, XBOOLE_0:def 5;

          then z in ( dom (PF . (k + 1))) by A10, MESFUNC1:def 3;

          then ((PF . (k + 1)) . z) = (((PF . k) . z) + ((F . (k + 1)) . z)) by A10, MESFUNC1:def 3;

          hence thesis by A5, A6, A11, NAT_1: 13, XXREAL_3: 16;

        end;

        (PF . 0 ) = (F . 0 ) by Def4;

        then

         A12: P[ 0 ] by A3;

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

        hence contradiction by A2;

      end;

      hence thesis;

    end;

    theorem :: MESFUNC9:24

    F is additive & z in ( dom (( Partial_Sums F) . n)) & ((( Partial_Sums F) . n) . z) = +infty & m <= n implies ((F . m) . z) <> -infty

    proof

      assume that

       A1: F is additive and

       A2: z in ( dom (( Partial_Sums F) . n)) and

       A3: ((( Partial_Sums F) . n) . z) = +infty and

       A4: m <= n;

      

       A5: z in ( dom (F . m)) by A2, A4, Th22;

      consider k be Nat such that

       A6: k <= n and

       A7: ((F . k) . z) = +infty by A2, A3, Th23;

      z in ( dom (F . k)) by A2, A6, Th22;

      then z in (( dom (F . m)) /\ ( dom (F . k))) by A5, XBOOLE_0:def 4;

      hence thesis by A1, A7;

    end;

    theorem :: MESFUNC9:25

    

     Th25: z in ( dom (( Partial_Sums F) . n)) & ((( Partial_Sums F) . n) . z) = -infty implies ex m be Nat st m <= n & ((F . m) . z) = -infty

    proof

      set PF = ( Partial_Sums F);

      assume that

       A1: z in ( dom (PF . n)) and

       A2: ((PF . n) . z) = -infty ;

      now

        defpred P[ Nat] means $1 <= n implies ((PF . $1) . z) <> -infty ;

        assume

         A3: for m be Nat st m <= n holds ((F . m) . z) <> -infty ;

        

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

        proof

          let k be Nat;

          assume

           A5: P[k];

          assume

           A6: (k + 1) <= n;

          then k <= n by NAT_1: 13;

          then

           A7: z in ( dom (PF . k)) by A1, Th22;

           not ((PF . k) . z) in { -infty } by A5, A6, NAT_1: 13, TARSKI:def 1;

          then not z in ((PF . k) " { -infty }) by FUNCT_1:def 7;

          then

           A8: not z in (((PF . k) " { -infty }) /\ ((F . (k + 1)) " { +infty })) by XBOOLE_0:def 4;

          z in ( dom (F . (k + 1))) by A1, A6, Th22;

          then

           A9: z in (( dom (PF . k)) /\ ( dom (F . (k + 1)))) by A7, XBOOLE_0:def 4;

          

           A10: (PF . (k + 1)) = ((PF . k) + (F . (k + 1))) by Def4;

          

           A11: ((F . (k + 1)) . z) <> -infty by A3, A6;

          then not ((F . (k + 1)) . z) in { -infty } by TARSKI:def 1;

          then not z in ((F . (k + 1)) " { -infty }) by FUNCT_1:def 7;

          then not z in (((PF . k) " { +infty }) /\ ((F . (k + 1)) " { -infty })) by XBOOLE_0:def 4;

          then not z in ((((PF . k) " { -infty }) /\ ((F . (k + 1)) " { +infty })) \/ (((PF . k) " { +infty }) /\ ((F . (k + 1)) " { -infty }))) by A8, XBOOLE_0:def 3;

          then z in ((( dom (PF . k)) /\ ( dom (F . (k + 1)))) \ ((((PF . k) " { -infty }) /\ ((F . (k + 1)) " { +infty })) \/ (((PF . k) " { +infty }) /\ ((F . (k + 1)) " { -infty })))) by A9, XBOOLE_0:def 5;

          then z in ( dom (PF . (k + 1))) by A10, MESFUNC1:def 3;

          then ((PF . (k + 1)) . z) = (((PF . k) . z) + ((F . (k + 1)) . z)) by A10, MESFUNC1:def 3;

          hence thesis by A5, A6, A11, NAT_1: 13, XXREAL_3: 17;

        end;

        (PF . 0 ) = (F . 0 ) by Def4;

        then

         A12: P[ 0 ] by A3;

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

        hence contradiction by A2;

      end;

      hence thesis;

    end;

    theorem :: MESFUNC9:26

    F is additive & z in ( dom (( Partial_Sums F) . n)) & ((( Partial_Sums F) . n) . z) = -infty & m <= n implies ((F . m) . z) <> +infty

    proof

      assume

       A1: F is additive;

      assume that

       A2: z in ( dom (( Partial_Sums F) . n)) and

       A3: ((( Partial_Sums F) . n) . z) = -infty ;

      assume m <= n;

      then

       A4: z in ( dom (F . m)) by A2, Th22;

      consider k be Nat such that

       A5: k <= n and

       A6: ((F . k) . z) = -infty by A2, A3, Th25;

      z in ( dom (F . k)) by A2, A5, Th22;

      then z in (( dom (F . m)) /\ ( dom (F . k))) by A4, XBOOLE_0:def 4;

      hence thesis by A1, A6;

    end;

    theorem :: MESFUNC9:27

    

     Th27: F is additive implies (((( Partial_Sums F) . n) " { -infty }) /\ ((F . (n + 1)) " { +infty })) = {} & (((( Partial_Sums F) . n) " { +infty }) /\ ((F . (n + 1)) " { -infty })) = {}

    proof

      set PF = ( Partial_Sums F);

      assume

       A1: F is additive;

      now

        given z be object such that

         A2: z in ((PF . n) " { -infty }) and

         A3: z in ((F . (n + 1)) " { +infty });

        

         A4: z in ( dom (PF . n)) by A2, FUNCT_1:def 7;

        ((PF . n) . z) in { -infty } by A2, FUNCT_1:def 7;

        then ((PF . n) . z) = -infty by TARSKI:def 1;

        then

        consider k be Nat such that

         A5: k <= n and

         A6: ((F . k) . z) = -infty by A4, Th25;

        

         A7: z in ( dom (F . (n + 1))) by A3, FUNCT_1:def 7;

        ((F . (n + 1)) . z) in { +infty } by A3, FUNCT_1:def 7;

        then

         A8: ((F . (n + 1)) . z) = +infty by TARSKI:def 1;

        z in ( dom (F . k)) by A4, A5, Th22;

        then z in (( dom (F . k)) /\ ( dom (F . (n + 1)))) by A7, XBOOLE_0:def 4;

        hence contradiction by A1, A8, A6;

      end;

      then ((PF . n) " { -infty }) misses ((F . (n + 1)) " { +infty }) by XBOOLE_0: 3;

      hence (((PF . n) " { -infty }) /\ ((F . (n + 1)) " { +infty })) = {} by XBOOLE_0:def 7;

      now

        given z be object such that

         A9: z in ((PF . n) " { +infty }) and

         A10: z in ((F . (n + 1)) " { -infty });

        

         A11: z in ( dom (PF . n)) by A9, FUNCT_1:def 7;

        ((PF . n) . z) in { +infty } by A9, FUNCT_1:def 7;

        then ((PF . n) . z) = +infty by TARSKI:def 1;

        then

        consider k be Nat such that

         A12: k <= n and

         A13: ((F . k) . z) = +infty by A11, Th23;

        

         A14: z in ( dom (F . (n + 1))) by A10, FUNCT_1:def 7;

        ((F . (n + 1)) . z) in { -infty } by A10, FUNCT_1:def 7;

        then

         A15: ((F . (n + 1)) . z) = -infty by TARSKI:def 1;

        z in ( dom (F . k)) by A11, A12, Th22;

        then z in (( dom (F . k)) /\ ( dom (F . (n + 1)))) by A14, XBOOLE_0:def 4;

        hence contradiction by A1, A15, A13;

      end;

      then ((PF . n) " { +infty }) misses ((F . (n + 1)) " { -infty }) by XBOOLE_0: 3;

      hence thesis by XBOOLE_0:def 7;

    end;

    theorem :: MESFUNC9:28

    

     Th28: F is additive implies ( dom (( Partial_Sums F) . n)) = ( meet { ( dom (F . k)) where k be Element of NAT : k <= n })

    proof

      deffunc DOM1( Nat) = { ( dom (F . k)) where k be Element of NAT : k <= $1 };

      set PF = ( Partial_Sums F);

      defpred P[ Nat] means ( dom (PF . $1)) = ( meet { ( dom (F . k)) where k be Element of NAT : k <= $1 });

      

       A1: ( dom (PF . 0 )) = ( dom (F . 0 )) by Def4;

      now

        let V be object;

        assume V in DOM1(0);

        then

        consider k be Element of NAT such that

         A2: V = ( dom (F . k)) and

         A3: k <= 0 ;

        k = 0 by A3;

        hence V in {( dom (F . 0 ))} by A2, TARSKI:def 1;

      end;

      then

       A4: DOM1(0) c= {( dom (F . 0 ))};

      assume

       A5: F is additive;

      

       A6: for m be Nat st P[m] holds P[(m + 1)]

      proof

        let m be Nat;

        

         A7: (PF . (m + 1)) = ((PF . m) + (F . (m + 1))) by Def4;

        

         A8: (((PF . m) " { +infty }) /\ ((F . (m + 1)) " { -infty })) = {} by A5, Th27;

        

         A9: ( dom (F . 0 )) in DOM1(+);

        now

          let V be object;

          assume

           A10: V in (( meet DOM1(m)) /\ ( dom (F . (m + 1))));

          then

           A11: V in ( dom (F . (m + 1))) by XBOOLE_0:def 4;

          

           A12: V in ( meet DOM1(m)) by A10, XBOOLE_0:def 4;

          for W be set holds W in DOM1(+) implies V in W

          proof

            let W be set;

            assume W in DOM1(+);

            then

            consider i be Element of NAT such that

             A13: W = ( dom (F . i)) and

             A14: i <= (m + 1);

            now

              assume i <= m;

              then W in DOM1(m) by A13;

              hence thesis by A12, SETFAM_1:def 1;

            end;

            hence thesis by A11, A13, A14, NAT_1: 8;

          end;

          hence V in ( meet DOM1(+)) by A9, SETFAM_1:def 1;

        end;

        then

         A15: (( meet DOM1(m)) /\ ( dom (F . (m + 1)))) c= ( meet DOM1(+));

        

         A16: ( dom (F . 0 )) in DOM1(m);

        now

          now

            let V be object;

            assume V in DOM1(m);

            then

            consider i be Element of NAT such that

             A17: V = ( dom (F . i)) and

             A18: i <= m;

            i <= (m + 1) by A18, NAT_1: 12;

            hence V in DOM1(+) by A17;

          end;

          then DOM1(m) c= DOM1(+);

          then

           A19: ( meet DOM1(+)) c= ( meet DOM1(m)) by A16, SETFAM_1: 6;

          let V be object;

          assume

           A20: V in ( meet DOM1(+));

          ( dom (F . (m + 1))) in DOM1(+);

          then V in ( dom (F . (m + 1))) by A20, SETFAM_1:def 1;

          hence V in (( meet DOM1(m)) /\ ( dom (F . (m + 1)))) by A20, A19, XBOOLE_0:def 4;

        end;

        then

         A21: ( meet DOM1(+)) c= (( meet DOM1(m)) /\ ( dom (F . (m + 1))));

        (((PF . m) " { -infty }) /\ ((F . (m + 1)) " { +infty })) = {} by A5, Th27;

        then

         A22: ( dom (PF . (m + 1))) = ((( dom (PF . m)) /\ ( dom (F . (m + 1)))) \ ( {} \/ {} )) by A8, A7, MESFUNC1:def 3;

        assume P[m];

        hence thesis by A22, A21, A15, XBOOLE_0:def 10;

      end;

      now

        let V be object;

        assume V in {( dom (F . 0 ))};

        then V = ( dom (F . 0 )) by TARSKI:def 1;

        hence V in DOM1(0);

      end;

      then {( dom (F . 0 ))} c= DOM1(0);

      then DOM1(0) = {( dom (F . 0 ))} by A4, XBOOLE_0:def 10;

      then

       A23: P[ 0 ] by A1, SETFAM_1: 10;

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

      hence thesis;

    end;

    theorem :: MESFUNC9:29

    

     Th29: F is additive & F is with_the_same_dom implies ( dom (( Partial_Sums F) . n)) = ( dom (F . 0 ))

    proof

      assume that

       A1: F is additive and

       A2: F is with_the_same_dom;

      now

        let D be object;

        

         A3: ( dom (F . 0 )) in { ( dom (F . k)) where k be Element of NAT : k <= n };

        assume D in ( meet { ( dom (F . k)) where k be Element of NAT : k <= n });

        then D in ( dom (F . 0 )) by A3, SETFAM_1:def 1;

        hence D in ( meet {( dom (F . 0 ))}) by SETFAM_1: 10;

      end;

      then

       A4: ( meet { ( dom (F . k)) where k be Element of NAT : k <= n }) c= ( meet {( dom (F . 0 ))});

      now

        let D be object;

        assume D in ( meet {( dom (F . 0 ))});

        then

         A5: D in ( dom (F . 0 )) by SETFAM_1: 10;

        

         A6: for E be set holds E in { ( dom (F . k)) where k be Element of NAT : k <= n } implies D in E

        proof

          let E be set;

          assume E in { ( dom (F . k)) where k be Element of NAT : k <= n };

          then ex k1 be Element of NAT st E = ( dom (F . k1)) & k1 <= n;

          hence thesis by A2, A5;

        end;

        ( dom (F . 0 )) in { ( dom (F . k)) where k be Element of NAT : k <= n };

        hence D in ( meet { ( dom (F . k)) where k be Element of NAT : k <= n }) by A6, SETFAM_1:def 1;

      end;

      then ( meet {( dom (F . 0 ))}) c= ( meet { ( dom (F . k)) where k be Element of NAT : k <= n });

      then ( meet { ( dom (F . k)) where k be Element of NAT : k <= n }) = ( meet {( dom (F . 0 ))}) by A4, XBOOLE_0:def 10;

      then ( dom (( Partial_Sums F) . n)) = ( meet {( dom (F . 0 ))}) by A1, Th28;

      hence thesis by SETFAM_1: 10;

    end;

    theorem :: MESFUNC9:30

    

     Th30: (for n be Nat holds (F . n) is nonnegative) implies F is additive by SUPINF_2: 51;

    theorem :: MESFUNC9:31

    

     Th31: F is additive & (for n holds (G . n) = ((F . n) | D)) implies G is additive

    proof

      assume that

       A1: F is additive and

       A2: for n holds (G . n) = ((F . n) | D);

      let n,m be Nat;

      

       A3: (G . m) = ((F . m) | D) by A2;

      then

       A4: ( dom (G . m)) c= ( dom (F . m)) by RELAT_1: 60;

      assume n <> m;

      let x be set;

      assume

       A5: x in (( dom (G . n)) /\ ( dom (G . m)));

      then

       A6: x in ( dom (G . m)) by XBOOLE_0:def 4;

      

       A7: (G . n) = ((F . n) | D) by A2;

      then ( dom (G . n)) c= ( dom (F . n)) by RELAT_1: 60;

      then (( dom (G . n)) /\ ( dom (G . m))) c= (( dom (F . n)) /\ ( dom (F . m))) by A4, XBOOLE_1: 27;

      then

       A8: ((F . n) . x) <> +infty or ((F . m) . x) <> -infty by A1, A5;

      x in ( dom (G . n)) by A5, XBOOLE_0:def 4;

      hence thesis by A7, A3, A8, A6, FUNCT_1: 47;

    end;

    theorem :: MESFUNC9:32

    

     Th32: F is additive & F is with_the_same_dom & D c= ( dom (F . 0 )) & x in D implies (( Partial_Sums (F # x)) . n) = ((( Partial_Sums F) # x) . n)

    proof

      set PF = ( Partial_Sums F);

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

      assume that

       A1: F is additive and

       A2: F is with_the_same_dom and

       A3: D c= ( dom (F . 0 )) and

       A4: x in D;

      defpred P[ Nat] means (PFx . $1) = ((PF # x) . $1);

      

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

      proof

        let k be Nat;

        assume

         A6: P[k];

        (PFx . (k + 1)) = ((PFx . k) + ((F # x) . (k + 1))) by Def1;

        then (PFx . (k + 1)) = (((PF # x) . k) + ((F . (k + 1)) . x)) by A6, MESFUNC5:def 13;

        then

         A7: (PFx . (k + 1)) = (((PF . k) . x) + ((F . (k + 1)) . x)) by MESFUNC5:def 13;

        

         A8: (PF . (k + 1)) = ((PF . k) + (F . (k + 1))) by Def4;

        D c= ( dom (PF . (k + 1))) by A1, A2, A3, Th29;

        then (PFx . (k + 1)) = ((PF . (k + 1)) . x) by A4, A8, A7, MESFUNC1:def 3;

        hence thesis by MESFUNC5:def 13;

      end;

      (PFx . 0 ) = ((F # x) . 0 ) by Def1;

      then (PFx . 0 ) = ((F . 0 ) . x) by MESFUNC5:def 13;

      then (PFx . 0 ) = ((PF . 0 ) . x) by Def4;

      then

       A9: P[ 0 ] by MESFUNC5:def 13;

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

      hence thesis;

    end;

    theorem :: MESFUNC9:33

    

     Th33: F is additive & F is with_the_same_dom & D c= ( dom (F . 0 )) & x in D implies (( Partial_Sums (F # x)) is convergent_to_finite_number iff (( Partial_Sums F) # x) is convergent_to_finite_number) & (( Partial_Sums (F # x)) is convergent_to_+infty iff (( Partial_Sums F) # x) is convergent_to_+infty) & (( Partial_Sums (F # x)) is convergent_to_-infty iff (( Partial_Sums F) # x) is convergent_to_-infty) & (( Partial_Sums (F # x)) is convergent iff (( Partial_Sums F) # x) is convergent)

    proof

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

      set PF = ( Partial_Sums F);

      assume that

       A1: F is additive and

       A2: F is with_the_same_dom and

       A3: D c= ( dom (F . 0 )) and

       A4: x in D;

      now

        assume PFx is convergent_to_finite_number;

        then

        consider g be Real such that

         A6: for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((PFx . m) - g).| < p;

        now

          let p be Real;

          assume 0 < p;

          then

          consider n be Nat such that

           A7: for m be Nat st n <= m holds |.((PFx . m) - g).| < p by A6;

          take n;

          let m be Nat;

          assume

           A8: n <= m;

          (PFx . m) = ((PF # x) . m) by A1, A2, A3, A4, Th32;

          hence |.(((PF # x) . m) - g).| < p by A7, A8;

        end;

        hence (PF # x) is convergent_to_finite_number;

      end;

      now

        assume (PF # x) is convergent_to_finite_number;

        then

        consider g be Real such that

         A10: for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.(((PF # x) . m) - g).| < p;

        now

          let p be Real;

          assume 0 < p;

          then

          consider n be Nat such that

           A11: for m be Nat st n <= m holds |.(((PF # x) . m) - g).| < p by A10;

          take n;

          let m be Nat;

          assume

           A12: n <= m;

          (PFx . m) = ((PF # x) . m) by A1, A2, A3, A4, Th32;

          hence |.((PFx . m) - g).| < p by A11, A12;

        end;

        hence PFx is convergent_to_finite_number;

      end;

      now

        assume

         A14: PFx is convergent_to_+infty;

        now

          let r be Real;

          assume 0 < r;

          then

          consider n be Nat such that

           A15: for m be Nat st n <= m holds r <= (PFx . m) by A14;

          take n;

          let m be Nat;

          assume n <= m;

          then r <= (PFx . m) by A15;

          hence r <= ((PF # x) . m) by A1, A2, A3, A4, Th32;

        end;

        hence (PF # x) is convergent_to_+infty;

      end;

      now

        assume

         A17: (PF # x) is convergent_to_+infty;

        now

          let r be Real;

          assume 0 < r;

          then

          consider n be Nat such that

           A18: for m be Nat st n <= m holds r <= ((PF # x) . m) by A17;

          take n;

          let m be Nat;

          assume n <= m;

          then r <= ((PF # x) . m) by A18;

          hence r <= (PFx . m) by A1, A2, A3, A4, Th32;

        end;

        hence PFx is convergent_to_+infty;

      end;

      now

        assume

         A20: PFx is convergent_to_-infty;

        now

          let r be Real;

          assume r < 0 ;

          then

          consider n be Nat such that

           A21: for m be Nat st n <= m holds (PFx . m) <= r by A20;

          take n;

          let m be Nat;

          assume n <= m;

          then (PFx . m) <= r by A21;

          hence ((PF # x) . m) <= r by A1, A2, A3, A4, Th32;

        end;

        hence (PF # x) is convergent_to_-infty;

      end;

      now

        assume

         A23: (PF # x) is convergent_to_-infty;

        now

          let r be Real;

          assume r < 0 ;

          then

          consider n be Nat such that

           A24: for m be Nat st n <= m holds ((PF # x) . m) <= r by A23;

          take n;

          let m be Nat;

          assume n <= m;

          then ((PF # x) . m) <= r by A24;

          hence (PFx . m) <= r by A1, A2, A3, A4, Th32;

        end;

        hence PFx is convergent_to_-infty;

      end;

      hereby

        assume

         A25: PFx is convergent;

        per cases by A25;

          suppose PFx is convergent_to_+infty;

          hence (PF # x) is convergent by A13;

        end;

          suppose PFx is convergent_to_-infty;

          hence (PF # x) is convergent by A19;

        end;

          suppose PFx is convergent_to_finite_number;

          hence (PF # x) is convergent by A5;

        end;

      end;

      assume

       A26: (PF # x) is convergent;

      per cases by A26;

        suppose (PF # x) is convergent_to_+infty;

        hence thesis by A16;

      end;

        suppose (PF # x) is convergent_to_-infty;

        hence thesis by A22;

      end;

        suppose (PF # x) is convergent_to_finite_number;

        hence thesis by A9;

      end;

    end;

    theorem :: MESFUNC9:34

    

     Th34: F is additive & F is with_the_same_dom & ( dom f) c= ( dom (F . 0 )) & x in ( dom f) & (F # x) is summable & (f . x) = ( Sum (F # x)) implies (f . x) = ( lim (( Partial_Sums F) # x))

    proof

      set PF = ( Partial_Sums F);

      assume that

       A1: F is additive and

       A2: F is with_the_same_dom and

       A3: ( dom f) c= ( dom (F . 0 )) and

       A4: x in ( dom f) and

       A5: (F # x) is summable and

       A6: (f . x) = ( Sum (F # x));

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

      PFx is convergent by A5;

      then

       A7: (PF # x) is convergent by A1, A2, A3, A4, Th33;

      per cases by A7, MESFUNC5:def 12;

        suppose

         A8: ex g be Real st ( lim (PF # x)) = g & (for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.(((PF # x) . m) - ( lim (PF # x))).| < p) & (PF # x) is convergent_to_finite_number;

        then

         A9: PFx is convergent_to_finite_number by A1, A2, A3, A4, Th33;

        then

         A10: not PFx is convergent_to_+infty by MESFUNC5: 50;

        

         A11: not PFx is convergent_to_-infty by A9, MESFUNC5: 51;

        PFx is convergent by A9;

        then

         A12: ex g be Real st (f . x) = g & (for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((PFx . m) - (f . x)).| < p) & PFx is convergent_to_finite_number by A6, A10, A11, MESFUNC5:def 12;

        now

          let p be Real;

          assume 0 < p;

          then

          consider n be Nat such that

           A13: for m be Nat st n <= m holds |.((PFx . m) - (f . x)).| < p by A12;

          take n;

          let m be Nat;

          assume

           A14: n <= m;

          (PFx . m) = ((PF # x) . m) by A1, A2, A3, A4, Th32;

          hence |.(((PF # x) . m) - (f . x)).| < p by A13, A14;

        end;

        hence thesis by A7, A8, A12, MESFUNC5:def 12;

      end;

        suppose

         A15: ( lim (PF # x)) = +infty & (PF # x) is convergent_to_+infty;

        then

         A16: PFx is convergent_to_+infty by A1, A2, A3, A4, Th33;

        then PFx is convergent;

        hence thesis by A6, A15, A16, MESFUNC5:def 12;

      end;

        suppose

         A17: ( lim (PF # x)) = -infty & (PF # x) is convergent_to_-infty;

        then

         A18: PFx is convergent_to_-infty by A1, A2, A3, A4, Th33;

        then PFx is convergent;

        hence thesis by A6, A17, A18, MESFUNC5:def 12;

      end;

    end;

    theorem :: MESFUNC9:35

    

     Th35: (for m be Nat holds (F . m) is_simple_func_in S) implies F is additive & (( Partial_Sums F) . n) is_simple_func_in S

    proof

      defpred P[ Nat] means (( Partial_Sums F) . $1) is_simple_func_in S;

      assume

       A1: for m be Nat holds (F . m) is_simple_func_in S;

      hereby

        let n,m be Nat;

        assume n <> m;

        (F . n) is_simple_func_in S by A1;

        then (F . n) is without+infty by MESFUNC5: 14;

        hence for x be set st x in (( dom (F . n)) /\ ( dom (F . m))) holds ((F . n) . x) <> +infty or ((F . m) . x) <> -infty ;

      end;

      

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

      proof

        let k be Nat;

        assume

         A3: P[k];

        (F . (k + 1)) is_simple_func_in S by A1;

        then ((( Partial_Sums F) . k) + (F . (k + 1))) is_simple_func_in S by A3, MESFUNC5: 38;

        hence thesis by Def4;

      end;

      (( Partial_Sums F) . 0 ) = (F . 0 ) by Def4;

      then

       A4: P[ 0 ] by A1;

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

      hence thesis;

    end;

    theorem :: MESFUNC9:36

    

     Th36: (for m be Nat holds (F . m) is nonnegative) implies (( Partial_Sums F) . n) is nonnegative

    proof

      defpred P[ Nat] means (( Partial_Sums F) . $1) is nonnegative;

      assume

       A1: for m be Nat holds (F . m) is nonnegative;

       A2:

      now

        let k be Nat;

        assume

         A3: P[k];

        

         A4: (( Partial_Sums F) . (k + 1)) = ((( Partial_Sums F) . k) + (F . (k + 1))) by Def4;

        (F . (k + 1)) is nonnegative by A1;

        hence P[(k + 1)] by A3, A4, MESFUNC5: 22;

      end;

      (( Partial_Sums F) . 0 ) = (F . 0 ) by Def4;

      then

       A5: P[ 0 ] by A1;

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

      hence thesis;

    end;

    theorem :: MESFUNC9:37

    

     Th37: F is with_the_same_dom & x in ( dom (F . 0 )) & (for k be Nat holds (F . k) is nonnegative) & n <= m implies ((( Partial_Sums F) . n) . x) <= ((( Partial_Sums F) . m) . x)

    proof

      assume

       A1: F is with_the_same_dom;

      set PF = ( Partial_Sums F);

      assume

       A2: x in ( dom (F . 0 ));

      defpred P[ Nat] means ((PF . n) . x) <= ((PF . $1) . x);

      assume

       A3: for m be Nat holds (F . m) is nonnegative;

      

       A4: for k be Nat holds ((PF . k) . x) <= ((PF . (k + 1)) . x)

      proof

        let k be Nat;

        

         A5: (PF . (k + 1)) = ((PF . k) + (F . (k + 1))) by Def4;

        (F . (k + 1)) is nonnegative by A3;

        then

         A6: 0. <= ((F . (k + 1)) . x) by SUPINF_2: 39;

        ( dom (PF . (k + 1))) = ( dom (F . 0 )) by A1, A3, Th29, Th30;

        then ((PF . (k + 1)) . x) = (((PF . k) . x) + ((F . (k + 1)) . x)) by A2, A5, MESFUNC1:def 3;

        hence thesis by A6, XXREAL_3: 39;

      end;

      

       A7: for k be Nat st k >= n & (for l be Nat st l >= n & l < k holds P[l]) holds P[k]

      proof

        let k be Nat;

        assume that

         A8: k >= n and

         A9: for l be Nat st l >= n & l < k holds P[l];

        now

           A10:

          now

            assume

             A11: k > (n + 1);

            then

            reconsider l = (k - 1) as Element of NAT by NAT_1: 20;

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

            then

             A12: k > l by XREAL_1: 19;

            k = (l + 1);

            then

             A13: ((PF . l) . x) <= ((PF . k) . x) by A4;

            l >= n by A11, XREAL_1: 19;

            then ((PF . n) . x) <= ((PF . l) . x) by A9, A12;

            hence thesis by A13, XXREAL_0: 2;

          end;

          assume k > n;

          then k >= (n + 1) by NAT_1: 13;

          then k = (n + 1) or k > (n + 1) by XXREAL_0: 1;

          hence thesis by A4, A10;

        end;

        hence thesis by A8, XXREAL_0: 1;

      end;

      

       A14: for k be Nat st k >= n holds P[k] from NAT_1:sch 9( A7);

      assume n <= m;

      hence thesis by A14;

    end;

    theorem :: MESFUNC9:38

    

     Th38: F is with_the_same_dom & x in ( dom (F . 0 )) & (for m be Nat holds (F . m) is nonnegative) implies (( Partial_Sums F) # x) is non-decreasing & (( Partial_Sums F) # x) is convergent

    proof

      assume

       A1: F is with_the_same_dom;

      assume

       A2: x in ( dom (F . 0 ));

      assume

       A3: for m be Nat holds (F . m) is nonnegative;

      for n,m be Nat st m <= n holds ((( Partial_Sums F) # x) . m) <= ((( Partial_Sums F) # x) . n)

      proof

        let n,m be Nat;

        assume m <= n;

        then ((( Partial_Sums F) . m) . x) <= ((( Partial_Sums F) . n) . x) by A1, A2, A3, Th37;

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

        hence thesis by MESFUNC5:def 13;

      end;

      hence (( Partial_Sums F) # x) is non-decreasing by RINFSUP2: 7;

      hence thesis by RINFSUP2: 37;

    end;

    theorem :: MESFUNC9:39

    

     Th39: (for m be Nat holds (F . m) is without-infty) implies (( Partial_Sums F) . n) is without-infty

    proof

      defpred P[ Nat] means (( Partial_Sums F) . $1) is without-infty;

      assume

       A1: for m be Nat holds (F . m) is without-infty;

      

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

      proof

        let k be Nat;

        assume

         A3: P[k];

        

         A4: (F . (k + 1)) is without-infty by A1;

        (( Partial_Sums F) . (k + 1)) = ((( Partial_Sums F) . k) + (F . (k + 1))) by Def4;

        hence thesis by A3, A4, Th3;

      end;

      (( Partial_Sums F) . 0 ) = (F . 0 ) by Def4;

      then

       A5: P[ 0 ] by A1;

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

      hence thesis;

    end;

    theorem :: MESFUNC9:40

    (for m be Nat holds (F . m) is without+infty) implies (( Partial_Sums F) . n) is without+infty

    proof

      defpred P[ Nat] means (( Partial_Sums F) . $1) is without+infty;

      assume

       A1: for m be Nat holds (F . m) is without+infty;

      

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

      proof

        let k be Nat;

        assume

         A3: P[k];

        

         A4: (F . (k + 1)) is without+infty by A1;

        (( Partial_Sums F) . (k + 1)) = ((( Partial_Sums F) . k) + (F . (k + 1))) by Def4;

        hence thesis by A3, A4, Th4;

      end;

      (( Partial_Sums F) . 0 ) = (F . 0 ) by Def4;

      then

       A5: P[ 0 ] by A1;

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

      hence thesis;

    end;

    theorem :: MESFUNC9:41

    

     Th41: (for n be Nat holds (F . n) is E -measurable & (F . n) is without-infty) implies (( Partial_Sums F) . m) is E -measurable

    proof

      set PF = ( Partial_Sums F);

      defpred P[ Nat] means (PF . $1) is E -measurable;

      assume

       A1: for n be Nat holds (F . n) is E -measurable & (F . n) is without-infty;

      

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

      proof

        let k be Nat;

        assume

         A3: P[k];

        

         A4: (F . (k + 1)) is E -measurable by A1;

        

         A5: (F . (k + 1)) is without-infty by A1;

        (PF . k) is without-infty by A1, Th39;

        then ((PF . k) + (F . (k + 1))) is E -measurable by A3, A4, A5, MESFUNC5: 31;

        hence thesis by Def4;

      end;

      (PF . 0 ) = (F . 0 ) by Def4;

      then

       A6: P[ 0 ] by A1;

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

      hence thesis;

    end;

    theorem :: MESFUNC9:42

    

     Th42: F is additive & F is with_the_same_dom & G is additive & G is with_the_same_dom & x in (( dom (F . 0 )) /\ ( dom (G . 0 ))) & (for k be Nat, y be Element of X st y in (( dom (F . 0 )) /\ ( dom (G . 0 ))) holds ((F . k) . y) <= ((G . k) . y)) implies ((( Partial_Sums F) . n) . x) <= ((( Partial_Sums G) . n) . x)

    proof

      assume that

       A1: F is additive and

       A2: F is with_the_same_dom and

       A3: G is additive and

       A4: G is with_the_same_dom and

       A5: x in (( dom (F . 0 )) /\ ( dom (G . 0 ))) and

       A6: for k be Nat, y be Element of X st y in (( dom (F . 0 )) /\ ( dom (G . 0 ))) holds ((F . k) . y) <= ((G . k) . y);

      set PG = ( Partial_Sums G);

      set PF = ( Partial_Sums F);

      defpred P[ Nat] means ((PF . $1) . x) <= ((PG . $1) . x);

      

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

      proof

        let k be Nat;

        assume

         A8: P[k];

        ( dom (PF . (k + 1))) = ( dom (F . 0 )) by A1, A2, Th29;

        then

         A9: x in ( dom (PF . (k + 1))) by A5, XBOOLE_0:def 4;

        ( dom (PG . (k + 1))) = ( dom (G . 0 )) by A3, A4, Th29;

        then

         A10: x in ( dom (PG . (k + 1))) by A5, XBOOLE_0:def 4;

        (PG . (k + 1)) = ((PG . k) + (G . (k + 1))) by Def4;

        then

         A11: ((PG . (k + 1)) . x) = (((PG . k) . x) + ((G . (k + 1)) . x)) by A10, MESFUNC1:def 3;

        (PF . (k + 1)) = ((PF . k) + (F . (k + 1))) by Def4;

        then

         A12: ((PF . (k + 1)) . x) = (((PF . k) . x) + ((F . (k + 1)) . x)) by A9, MESFUNC1:def 3;

        ((F . (k + 1)) . x) <= ((G . (k + 1)) . x) by A5, A6;

        hence thesis by A8, A12, A11, XXREAL_3: 36;

      end;

      

       A13: (PG . 0 ) = (G . 0 ) by Def4;

      (PF . 0 ) = (F . 0 ) by Def4;

      then

       A14: P[ 0 ] by A5, A6, A13;

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

      hence thesis;

    end;

    theorem :: MESFUNC9:43

    

     Th43: for X be non empty set, F be Functional_Sequence of X, ExtREAL st F is additive & F is with_the_same_dom holds ( Partial_Sums F) is with_the_same_dom

    proof

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

      assume that

       A1: F is additive and

       A2: F is with_the_same_dom;

      let n,m be Nat;

      ( dom (( Partial_Sums F) . n)) = ( dom (F . 0 )) by A1, A2, Th29;

      hence thesis by A1, A2, Th29;

    end;

    theorem :: MESFUNC9:44

    

     Th44: ( dom (F . 0 )) = E & F is additive & F is with_the_same_dom & (for n be Nat holds (( Partial_Sums F) . n) is E -measurable) & (for x be Element of X st x in E holds (F # x) is summable) implies ( lim ( Partial_Sums F)) is E -measurable

    proof

      assume that

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

       A2: F is additive and

       A3: F is with_the_same_dom and

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

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

      reconsider PF = ( Partial_Sums F) as with_the_same_dom Functional_Sequence of X, ExtREAL by A2, A3, Th43;

       A6:

      now

        let x be Element of X;

        assume

         A7: x in E;

        then (F # x) is summable by A5;

        then ( Partial_Sums (F # x)) is convergent;

        hence (PF # x) is convergent by A1, A2, A3, A7, Th33;

      end;

      ( dom (( Partial_Sums F) . 0 )) = E by A1, A2, A3, Th29;

      hence thesis by A4, A6, MESFUNC8: 25;

    end;

    theorem :: MESFUNC9:45

    (for n be Nat holds (F . n) is_integrable_on M) implies for m be Nat holds (( Partial_Sums F) . m) is_integrable_on M

    proof

      set PF = ( Partial_Sums F);

      defpred P1[ Nat] means (PF . $1) is_integrable_on M;

      assume

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

      

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

      proof

        let k be Nat;

        assume

         A3: P1[k];

        (F . (k + 1)) is_integrable_on M by A1;

        then ((PF . k) + (F . (k + 1))) is_integrable_on M by A3, MESFUNC5: 108;

        hence thesis by Def4;

      end;

      (PF . 0 ) = (F . 0 ) by Def4;

      then

       A4: P1[ 0 ] by A1;

      thus for m be Nat holds P1[m] from NAT_1:sch 2( A4, A2);

    end;

    theorem :: MESFUNC9:46

    

     Th46: E = ( dom (F . 0 )) & F is additive & F is with_the_same_dom & (for n be Nat holds (F . n) is E -measurable & (F . n) is nonnegative & (I . n) = ( Integral (M,(F . n)))) implies ( Integral (M,(( Partial_Sums F) . m))) = (( Partial_Sums I) . m)

    proof

      assume that

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

       A2: F is additive and

       A3: F is with_the_same_dom and

       A4: for n be Nat holds (F . n) is E -measurable & (F . n) is nonnegative & (I . n) = ( Integral (M,(F . n)));

      set PF = ( Partial_Sums F);

      

       A5: for n be Nat holds (F . n) is without-infty by A4, MESFUNC5: 12;

      thus ( Integral (M,(( Partial_Sums F) . m))) = (( Partial_Sums I) . m)

      proof

        set PI = ( Partial_Sums I);

        defpred P2[ Nat] means ( Integral (M,(PF . $1))) = (( Partial_Sums I) . $1);

        

         A6: for k be Nat st P2[k] holds P2[(k + 1)]

        proof

          let k be Nat;

          assume

           A7: P2[k];

          

           A8: (F . (k + 1)) is E -measurable by A4;

          

           A9: ( dom (F . (k + 1))) = E by A1, A3;

          

           A10: (PF . (k + 1)) is E -measurable by A4, A5, Th41;

          

           A11: (PF . (k + 1)) is nonnegative by A4, Th36;

          

           A12: (F . (k + 1)) is nonnegative by A4;

          

           A13: (PF . k) is nonnegative by A4, Th36;

          

           A14: ( dom (PF . k)) = E by A1, A2, A3, Th29;

          

           A15: (PF . k) is E -measurable by A4, A5, Th41;

          then

          consider D be Element of S such that

           A16: D = ( dom ((PF . k) + (F . (k + 1)))) and

           A17: ( integral+ (M,((PF . k) + (F . (k + 1))))) = (( integral+ (M,((PF . k) | D))) + ( integral+ (M,((F . (k + 1)) | D)))) by A14, A9, A8, A13, A12, MESFUNC5: 78;

          

           A18: D = (E /\ E) by A14, A9, A13, A12, A16, MESFUNC5: 22;

          then

           A19: ((PF . k) | D) = (PF . k) by A14;

          

           A20: ((F . (k + 1)) | D) = (F . (k + 1)) by A9, A18;

          ( dom (PF . (k + 1))) = E by A1, A2, A3, Th29;

          

          then ( Integral (M,(PF . (k + 1)))) = ( integral+ (M,(PF . (k + 1)))) by A10, A11, MESFUNC5: 88

          .= (( integral+ (M,((PF . k) | D))) + ( integral+ (M,((F . (k + 1)) | D)))) by A17, Def4

          .= (( Integral (M,(PF . k))) + ( integral+ (M,((F . (k + 1)) | D)))) by A14, A15, A13, A19, MESFUNC5: 88

          .= (( Integral (M,(PF . k))) + ( Integral (M,(F . (k + 1))))) by A9, A8, A12, A20, MESFUNC5: 88

          .= ((PI . k) + (I . (k + 1))) by A4, A7;

          hence thesis by Def1;

        end;

        ( Integral (M,(PF . 0 ))) = ( Integral (M,(F . 0 ))) by Def4;

        then ( Integral (M,(PF . 0 ))) = (I . 0 ) by A4;

        then

         A21: P2[ 0 ] by Def1;

        for k be Nat holds P2[k] from NAT_1:sch 2( A21, A6);

        hence thesis;

      end;

    end;

    begin

    

     Lm2: E c= ( dom f) & f is E -measurable & E = {} & (for n be Nat holds (F . n) is_simple_func_in S) implies ex I be ExtREAL_sequence st (for n be Nat holds (I . n) = ( Integral (M,((F . n) | E)))) & I is summable & ( Integral (M,(f | E))) = ( Sum I)

    proof

      assume that

       A1: E c= ( dom f) and

       A2: f is E -measurable and

       A3: E = {} and

       A4: for n be Nat holds (F . n) is_simple_func_in S;

      take I = ( NAT --> 0. );

      

       A5: (M . E) = 0 by A3, VALUED_0:def 19;

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

      proof

        let n be Nat;

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

        reconsider D = ( dom (F . m)) as Element of S by A4, MESFUNC5: 37;

        (F . m) is D -measurable by A4, MESFUNC2: 34;

        then ( Integral (M,((F . m) | E))) = 0 by A5, MESFUNC5: 94;

        hence thesis by FUNCOP_1: 7;

      end;

      defpred P[ Nat] means (( Partial_Sums I) . $1) = 0 ;

      

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

      proof

        let k be Nat;

        assume

         A7: P[k];

        

         A8: (I . (k + 1)) = 0 by FUNCOP_1: 7;

        (( Partial_Sums I) . (k + 1)) = ((( Partial_Sums I) . k) + (I . (k + 1))) by Def1;

        hence thesis by A7, A8;

      end;

      (( Partial_Sums I) . 0 ) = (I . 0 ) by Def1;

      then

       A9: P[ 0 ] by FUNCOP_1: 7;

      

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

      

       A11: for n be Nat holds (( Partial_Sums I) . n) = 0 by A10;

      then

       A12: ( lim ( Partial_Sums I)) = 0 by MESFUNC5: 52;

      ( Partial_Sums I) is convergent_to_finite_number by A11, MESFUNC5: 52;

      then ( Partial_Sums I) is convergent;

      hence I is summable;

      

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

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

      then ( Integral (M,((f | E) | E))) = 0 by A2, A5, A13, MESFUNC5: 42, MESFUNC5: 94;

      hence thesis by A12;

    end;

    

     Lm3: E c= ( dom f) & f is nonnegative & f is E -measurable & F is additive & E common_on_dom F & (for n be Nat holds (F . n) is_simple_func_in S & (F . n) is nonnegative) & (for x be Element of X st x in E holds (F # x) is summable & (f . x) = ( Sum (F # x))) implies ex I be ExtREAL_sequence st (for n be Nat holds (I . n) = ( Integral (M,((F . n) | E)))) & I is summable & ( Integral (M,(f | E))) = ( Sum I)

    proof

      assume that

       A1: E c= ( dom f) and

       A2: f is nonnegative and

       A3: f is E -measurable and

       A4: F is additive and

       A5: E common_on_dom F and

       A6: for n be Nat holds (F . n) is_simple_func_in S & (F . n) is nonnegative and

       A7: for x be Element of X st x in E holds (F # x) is summable & (f . x) = ( Sum (F # x));

      deffunc G1( Nat) = ((F . $1) | E);

      consider g1 be Functional_Sequence of X, ExtREAL such that

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

      

       A9: for n be Nat holds ((F . n) | E) is_simple_func_in S & ((F . n) | E) is nonnegative & ( dom ((F . n) | E)) = E

      proof

        let n be Nat;

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

        thus ((F . n) | E) is_simple_func_in S by A6, MESFUNC5: 34;

        thus ((F . n) | E) is nonnegative by A6, MESFUNC5: 15;

        E c= ( dom (F . n9)) by A5, SEQFUNC:def 9;

        hence thesis by RELAT_1: 62;

      end;

      for n,m be Nat holds ( dom (g1 . n)) = ( dom (g1 . m))

      proof

        let n,m be Nat;

        ( dom (g1 . m)) = ( dom ((F . m) | E)) by A8;

        then

         A10: ( dom (g1 . m)) = E by A9;

        ( dom (g1 . n)) = ( dom ((F . n) | E)) by A8;

        hence thesis by A9, A10;

      end;

      then

       A11: g1 is with_the_same_dom;

      set G = ( Partial_Sums g1);

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

      consider I be ExtREAL_sequence such that

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

      take I;

      

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

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

      then

       A14: (f | E) is E -measurable by A3, MESFUNC5: 42;

      set L = ( Partial_Sums I);

      

       A15: for n be Nat holds (I . n) = ( Integral (M,((F . n) | E)))

      proof

        let n be Nat;

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

        (I . m) = ( Integral (M,(g1 . m))) by A12;

        hence thesis by A8;

      end;

      

       A16: for k be Nat holds (g1 . k) is nonnegative

      proof

        let k be Nat;

        ((F . k) | E) is nonnegative by A9;

        hence thesis by A8;

      end;

      

       A17: for n be Nat holds (G . n) is_simple_func_in S & (G . n) is nonnegative & ( dom (G . n)) = E

      proof

        let n be Nat;

        

         A18: for n be Nat holds (g1 . n) is_simple_func_in S

        proof

          let n be Nat;

          ((F . n) | E) is_simple_func_in S by A9;

          hence thesis by A8;

        end;

        hence (G . n) is_simple_func_in S by Th35;

        thus (G . n) is nonnegative by A16, Th36;

        ( dom (g1 . 0 )) = ( dom ((F . 0 ) | E)) by A8;

        then ( dom (g1 . 0 )) = E by A9;

        hence thesis by A11, A18, Th29, Th35;

      end;

      (G . 0 ) = (g1 . 0 ) by Def4;

      then

       A19: (G . 0 ) = ((F . 0 ) | E) by A8;

      

       A20: for n be Nat holds ( integral' (M,(G . n))) = (L . n)

      proof

        defpred L[ Nat] means (L . $1) = ( integral' (M,(G . $1)));

        let n be Nat;

        

         A21: (G . 0 ) is nonnegative by A17;

        

         A22: for k be Nat st L[k] holds L[(k + 1)]

        proof

          let k be Nat;

          assume

           A23: L[k];

          (L . (k + 1)) = ((( Partial_Sums I) . k) + (I . (k + 1))) by Def1;

          then

           A24: (L . (k + 1)) = (( integral' (M,(G . k))) + ( Integral (M,((F . (k + 1)) | E)))) by A15, A23;

          

           A25: ((F . (k + 1)) | E) is_simple_func_in S by A9;

          

           A26: ( dom ((F . (k + 1)) | E)) = E by A9;

          

           A27: (G . k) is_simple_func_in S by A17;

          (G . (k + 1)) = ((G . k) + (g1 . (k + 1))) by Def4;

          then

           A28: (G . (k + 1)) = ((G . k) + ((F . (k + 1)) | E)) by A8;

          

           A29: ((F . (k + 1)) | E) is nonnegative by A9;

          

           A30: (G . k) is nonnegative by A17;

          

           A31: ( dom (G . k)) = E by A17;

          then E = (( dom (G . k)) /\ ( dom ((F . (k + 1)) | E))) by A26;

          then ( dom ((G . k) + ((F . (k + 1)) | E))) = E by A25, A29, A27, A30, MESFUNC5: 65;

          then

           A32: ( integral' (M,((G . k) + ((F . (k + 1)) | E)))) = (( integral' (M,((G . k) | E))) + ( integral' (M,(((F . (k + 1)) | E) | E)))) by A25, A29, A27, A30, MESFUNC5: 65;

          ((G . k) | E) = (G . k) by A31;

          hence thesis by A28, A24, A25, A29, A32, MESFUNC5: 89;

        end;

        (L . 0 ) = (I . 0 ) by Def1;

        then

         A33: (L . 0 ) = ( Integral (M,(G . 0 ))) by A15, A19;

        (G . 0 ) is_simple_func_in S by A17;

        then

         A34: L[ 0 ] by A33, A21, MESFUNC5: 89;

        

         A35: for k be Nat holds L[k] from NAT_1:sch 2( A34, A22);

        thus thesis by A35;

      end;

      (g1 . 0 ) = ((F . 0 ) | E) by A8;

      then

       A36: ( dom (g1 . 0 )) = E by A9;

      

       A37: for x be Element of X st x in ( dom (f | E)) holds (g1 # x) is summable & ((f | E) . x) = ( Sum (g1 # x))

      proof

        let x be Element of X;

        assume

         A38: x in ( dom (f | E));

        then

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

        

         A40: for n be object st n in NAT holds ((F # x) . n) = ((g1 # x) . n)

        proof

          let n be object;

          assume n in NAT ;

          then

          reconsider n1 = n as Nat;

          

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

          

           A42: ( dom ((F . n1) | E)) = E by A9;

          ((F . n1) | E) = (g1 . n1) by A8;

          then ((g1 . n1) . x) = ((F . n1) . x) by A13, A38, A42, FUNCT_1: 47;

          hence thesis by A41, MESFUNC5:def 13;

        end;

        

         A43: (f . x) = ( Sum (F # x)) by A7, A13, A38;

        (F # x) is summable by A7, A13, A38;

        hence thesis by A43, A39, A40, FUNCT_2: 12;

      end;

      

       A44: (f | E) is nonnegative by A2, MESFUNC5: 15;

      then

      consider F be Functional_Sequence of X, ExtREAL , K be ExtREAL_sequence such that

       A45: for n be Nat holds (F . n) is_simple_func_in S & ( dom (F . n)) = ( dom (f | E)) and

       A46: for n be Nat holds (F . n) is nonnegative and

       A47: for n,m be Nat st n <= m holds for x be Element of X st x in ( dom (f | E)) holds ((F . n) . x) <= ((F . m) . x) and

       A48: for x be Element of X st x in ( dom (f | E)) holds (F # x) is convergent & ( lim (F # x)) = ((f | E) . x) and

       A49: for n be Nat holds (K . n) = ( integral' (M,(F . n))) and K is convergent and

       A50: ( integral+ (M,(f | E))) = ( lim K) by A13, A14, MESFUNC5:def 15;

      

       A51: g1 is additive by A4, A8, Th31;

      

       A52: for x be Element of X st x in E holds (F # x) is convergent & (G # x) is convergent & ( lim (F # x)) = ( lim (G # x))

      proof

        let x be Element of X;

        assume

         A53: x in E;

        hence (F # x) is convergent by A13, A48;

        (g1 # x) is summable by A13, A37, A53;

        then ( Partial_Sums (g1 # x)) is convergent;

        hence (G # x) is convergent by A11, A51, A36, A53, Th33;

        

         A54: ((f | E) . x) = ( Sum (g1 # x)) by A13, A37, A53;

        (g1 # x) is summable by A13, A37, A53;

        then ( lim (G # x)) = ((f | E) . x) by A4, A13, A8, A11, A36, A53, A54, Th31, Th34;

        hence thesis by A13, A48, A53;

      end;

      

       A55: 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 A11, A16, A36, Th37;

      then

       A56: L is convergent by A13, A17, A20, A45, A46, A47, A49, A52, MESFUNC5: 76;

      ( lim L) = ( integral+ (M,(f | E))) by A13, A17, A20, A45, A46, A47, A49, A50, A55, A52, MESFUNC5: 76;

      hence thesis by A13, A15, A14, A44, A56, MESFUNC5: 88;

    end;

    theorem :: MESFUNC9:47

    E c= ( dom f) & f is nonnegative & f is E -measurable & F is additive & (for n holds (F . n) is_simple_func_in S & (F . n) is nonnegative & E c= ( dom (F . n))) & (for x st x in E holds (F # x) is summable & (f . x) = ( Sum (F # x))) implies ex I be ExtREAL_sequence st (for n holds (I . n) = ( Integral (M,((F . n) | E)))) & I is summable & ( Integral (M,(f | E))) = ( Sum I)

    proof

      assume that

       A1: E c= ( dom f) and

       A2: f is nonnegative and

       A3: f is E -measurable and

       A4: F is additive and

       A5: for n holds (F . n) is_simple_func_in S & (F . n) is nonnegative & E c= ( dom (F . n)) and

       A6: for x st x in E holds (F # x) is summable & (f . x) = ( Sum (F # x));

      per cases ;

        suppose E = {} ;

        hence thesis by A1, A3, A5, Lm2;

      end;

        suppose

         A7: E <> {} ;

        for n be Nat holds (F . n) is_simple_func_in S & (F . n) is nonnegative & E c= ( dom (F . n)) by A5;

        then E common_on_dom F by A7, SEQFUNC:def 9;

        hence thesis by A1, A2, A3, A4, A5, A6, Lm3;

      end;

    end;

    theorem :: MESFUNC9:48

    E c= ( dom f) & f is nonnegative & f is E -measurable implies ex g be Functional_Sequence of X, ExtREAL st g is additive & (for n be Nat holds (g . n) is_simple_func_in S & (g . n) is nonnegative & (g . n) is E -measurable) & (for x be Element of X st x in E holds (g # x) is summable & (f . x) = ( Sum (g # x))) & ex I be ExtREAL_sequence st (for n be Nat holds (I . n) = ( Integral (M,((g . n) | E)))) & I is summable & ( Integral (M,(f | E))) = ( Sum I)

    proof

      assume that

       A1: E c= ( dom f) and

       A2: f is nonnegative and

       A3: f is E -measurable;

      set F = (f | E);

      

       A4: ( dom F) = E by A1, RELAT_1: 62;

      E = (( dom f) /\ E) by A1, XBOOLE_1: 28;

      then F is E -measurable by A3, MESFUNC5: 42;

      then

      consider h be Functional_Sequence of X, ExtREAL such that

       A5: for n be Nat holds (h . n) is_simple_func_in S & ( dom (h . n)) = ( dom F) and

       A6: for n be Nat holds (h . n) is nonnegative and

       A7: for n,m be Nat st n <= m holds for x be Element of X st x in ( dom F) holds ((h . n) . x) <= ((h . m) . x) and

       A8: for x be Element of X st x in ( dom F) holds (h # x) is convergent & ( lim (h # x)) = (F . x) by A2, A4, MESFUNC5: 15, MESFUNC5: 64;

      defpred P[ Nat, set, set] means $3 = ((h . ($1 + 1)) - (h . $1));

      

       A9: for n be Nat holds for x be set holds ex y be set st P[n, x, y];

      consider g be Function such that

       A10: ( dom g) = NAT & (g . 0 ) = (h . 0 ) & for n be Nat holds P[n, (g . n), (g . (n + 1))] from RECDEF_1:sch 1( A9);

      now

        defpred IND[ Nat] means (g . $1) is PartFunc of X, ExtREAL ;

        let f be object;

        assume f in ( rng g);

        then

        consider m be object such that

         A11: m in ( dom g) and

         A12: f = (g . m) by FUNCT_1:def 3;

        reconsider m as Element of NAT by A10, A11;

        

         A13: for n be Nat st IND[n] holds IND[(n + 1)]

        proof

          let n be Nat;

          assume IND[n];

          (g . (n + 1)) = ((h . (n + 1)) - (h . n)) by A10;

          hence thesis;

        end;

        

         A14: IND[ 0 ] by A10;

        for n be Nat holds IND[n] from NAT_1:sch 2( A14, A13);

        then (g . m) is PartFunc of X, ExtREAL ;

        hence f in ( PFuncs (X, ExtREAL )) by A12, PARTFUN1: 45;

      end;

      then ( rng g) c= ( PFuncs (X, ExtREAL ));

      then

      reconsider g as Functional_Sequence of X, ExtREAL by A10, FUNCT_2:def 1, RELSET_1: 4;

      take g;

      

       A15: for n be Nat holds (g . n) is_simple_func_in S & (g . n) is nonnegative & (g . n) is E -measurable & E c= ( dom (g . n))

      proof

        let n be Nat;

        per cases ;

          suppose

           A16: n = 0 ;

          hence (g . n) is_simple_func_in S & (g . n) is nonnegative by A5, A6, A10;

          hence (g . n) is E -measurable by MESFUNC2: 34;

          thus thesis by A4, A5, A10, A16;

        end;

          suppose n <> 0 ;

          then

          consider m be Nat such that

           A17: n = (m + 1) by NAT_1: 6;

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

          

           A18: (g . n) = ((h . n) - (h . m)) by A10, A17;

          then

           A19: (g . n) = ((h . n) + ( - (h . m))) by MESFUNC2: 8;

          

           A20: (h . n) is_simple_func_in S by A5;

          then

           A21: (h . n) is without-infty by MESFUNC5: 14;

          

           A22: ( dom (h . n)) = ( dom F) by A5;

          (( - jj) (#) (h . m)) is_simple_func_in S by A5, MESFUNC5: 39;

          then

           A23: ( - (h . m)) is_simple_func_in S by MESFUNC2: 9;

          hence (g . n) is_simple_func_in S by A19, A20, MESFUNC5: 38;

          

           A24: (h . m) is_simple_func_in S by A5;

          then (h . m) is without+infty by MESFUNC5: 14;

          then

           A25: ( dom ((h . n) - (h . m))) = (( dom (h . n)) /\ ( dom (h . m))) by A21, MESFUNC5: 17;

          

           A26: ( dom (h . m)) = ( dom F) by A5;

          then for x be object st x in ( dom ((h . n) - (h . m))) holds ((h . m) . x) <= ((h . n) . x) by A7, A17, A25, A22, NAT_1: 11;

          hence (g . n) is nonnegative by A18, A20, A24, MESFUNC5: 40;

          thus (g . n) is E -measurable by A19, A20, A23, MESFUNC2: 34, MESFUNC5: 38;

          thus thesis by A4, A10, A17, A25, A22, A26;

        end;

      end;

      hence

       A27: g is additive by Th35;

      thus for n be Nat holds (g . n) is_simple_func_in S & (g . n) is nonnegative & (g . n) is E -measurable by A15;

       A28:

      now

        let x be Element of X;

        assume

         A29: x in E;

        then

         A30: (h # x) is convergent by A4, A8;

        

         A31: for m be Nat holds (( Partial_Sums (g # x)) . m) = ((h # x) . m)

        proof

          defpred P[ Nat] means (( Partial_Sums (g # x)) . $1) = ((h # x) . $1);

          let m be Nat;

          

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

          proof

            set Pgx = ( Partial_Sums (g # x));

            let k be Nat;

            assume P[k];

            then

             A33: (Pgx . k) = ((h . k) . x) by MESFUNC5:def 13;

            

             A34: ( dom (h . (k + 1))) = ( dom F) by A5;

            

             A35: (h . (k + 1)) is_simple_func_in S by A5;

            then

             A36: (h . (k + 1)) is without-infty by MESFUNC5: 14;

            then

             A37: -infty < ((h . (k + 1)) . x);

            (h . (k + 1)) is without+infty by A35, MESFUNC5: 14;

            then

             A38: ((h . (k + 1)) . x) < +infty ;

            

             A39: ( dom (h . k)) = ( dom F) by A5;

            

             A40: (h . k) is_simple_func_in S by A5;

            then

             A41: (h . k) is without+infty by MESFUNC5: 14;

            then

             A42: ((h . k) . x) < +infty ;

            (h . k) is without-infty by A40, MESFUNC5: 14;

            then

             A43: -infty < ((h . k) . x);

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

            reconsider hk1x = ((h . (k + 1)) . x) as Element of REAL by A37, A38, XXREAL_0: 14;

            

             A44: (g . (k + 1)) = ((h . (k + 1)) - (h . k)) by A10;

            reconsider hkx = ((h . k) . x) as Element of REAL by A43, A42, XXREAL_0: 14;

            (((h . (k + 1)) . x) - ((h . k) . x)) = (hk1x - hkx) by SUPINF_2: 3;

            then

             A45: ((((h . (k + 1)) . x) - ((h . k) . x)) + ((h . k) . x)) = ((hk1x - hkx) + hkx) by SUPINF_2: 1;

            (Pgx . (k + 1)) = ((Pgx . k) + ((g # x) . (k + 1))) by Def1;

            then

             A46: (Pgx . (k + 1)) = (((h . k) . x) + ((g . (k + 1)) . x)) by A33, MESFUNC5:def 13;

            ( dom ((h . (k + 1)) - (h . k))) = (( dom (h . (k + 1))) /\ ( dom (h . k))) by A36, A41, MESFUNC5: 17;

            then ((g . (k + 1)) . x) = (((h . (k + 1)) . x) - ((h . k) . x)) by A4, A29, A34, A39, A44, MESFUNC1:def 4;

            hence thesis by A46, A45, MESFUNC5:def 13;

          end;

          (( Partial_Sums (g # x)) . 0 ) = ((g # x) . 0 ) by Def1;

          then (( Partial_Sums (g # x)) . 0 ) = ((g . 0 ) . x) by MESFUNC5:def 13;

          then

           A47: P[ 0 ] by A10, MESFUNC5:def 13;

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

          hence thesis;

        end;

        

         A48: ( lim (h # x)) = (F . x) by A4, A8, A29;

        per cases by A30;

          suppose

           A49: (h # x) is convergent_to_finite_number;

          then

           A50: not (h # x) is convergent_to_-infty by MESFUNC5: 51;

           not (h # x) is convergent_to_+infty by A49, MESFUNC5: 50;

          then

          consider s be Real such that

           A51: ( lim (h # x)) = s and

           A52: for p be Real st 0 < p holds ex N be Nat st for m be Nat st N <= m holds |.(((h # x) . m) - ( lim (h # x))).| < p and (h # x) is convergent_to_finite_number by A30, A50, MESFUNC5:def 12;

          for p be Real st 0 < p holds ex N be Nat st for m be Nat st N <= m holds |.((( Partial_Sums (g # x)) . m) - s).| < p

          proof

            let p be Real;

            assume 0 < p;

            then

            consider N be Nat such that

             A53: for m be Nat st N <= m holds |.(((h # x) . m) - ( lim (h # x))).| < p by A52;

            take N;

            let m be Nat;

            assume N <= m;

            then |.(((h # x) . m) - ( lim (h # x))).| < p by A53;

            hence thesis by A31, A51;

          end;

          then

           A54: ( Partial_Sums (g # x)) is convergent_to_finite_number;

          then

           A55: ( Partial_Sums (g # x)) is convergent;

          hence (g # x) is summable;

          for p be Real st 0 < p holds ex N be Nat st for m be Nat st N <= m holds |.((( Partial_Sums (g # x)) . m) - ( lim (h # x))).| < p

          proof

            let p be Real;

            assume 0 < p;

            then

            consider N be Nat such that

             A56: for m be Nat st N <= m holds |.(((h # x) . m) - ( lim (h # x))).| < p by A52;

            take N;

            let m be Nat;

            assume N <= m;

            then |.(((h # x) . m) - ( lim (h # x))).| < p by A56;

            hence thesis by A31;

          end;

          then ( lim ( Partial_Sums (g # x))) = ( lim (h # x)) by A51, A54, A55, MESFUNC5:def 12;

          hence ( Sum (g # x)) = (f . x) by A29, A48, FUNCT_1: 49;

        end;

          suppose

           A57: (h # x) is convergent_to_+infty;

          for p be Real st 0 < p holds ex N be Nat st for m be Nat st N <= m holds p <= (( Partial_Sums (g # x)) . m)

          proof

            let p be Real;

            assume 0 < p;

            then

            consider N be Nat such that

             A58: for m be Nat st N <= m holds p <= ((h # x) . m) by A57;

            take N;

            let m be Nat;

            assume N <= m;

            then p <= ((h # x) . m) by A58;

            hence thesis by A31;

          end;

          then

           A59: ( Partial_Sums (g # x)) is convergent_to_+infty;

          then

           A60: ( Partial_Sums (g # x)) is convergent;

          then

           A61: ( lim ( Partial_Sums (g # x))) = +infty by A59, MESFUNC5:def 12;

          thus (g # x) is summable by A60;

          ( lim (h # x)) = +infty by A30, A57, MESFUNC5:def 12;

          hence ( Sum (g # x)) = (f . x) by A29, A48, A61, FUNCT_1: 49;

        end;

          suppose

           A62: (h # x) is convergent_to_-infty;

          for p be Real st p < 0 holds ex N be Nat st for m be Nat st N <= m holds (( Partial_Sums (g # x)) . m) <= p

          proof

            let p be Real;

            assume p < 0 ;

            then

            consider N be Nat such that

             A63: for m be Nat st N <= m holds ((h # x) . m) <= p by A62;

            take N;

            let m be Nat;

            assume N <= m;

            then ((h # x) . m) <= p by A63;

            hence thesis by A31;

          end;

          then

           A64: ( Partial_Sums (g # x)) is convergent_to_-infty;

          then

           A65: ( Partial_Sums (g # x)) is convergent;

          then

           A66: ( lim ( Partial_Sums (g # x))) = -infty by A64, MESFUNC5:def 12;

          thus (g # x) is summable by A65;

          ( lim (h # x)) = -infty by A30, A62, MESFUNC5:def 12;

          hence ( Sum (g # x)) = (f . x) by A29, A48, A66, FUNCT_1: 49;

        end;

      end;

      hence for x be Element of X st x in E holds (g # x) is summable & (f . x) = ( Sum (g # x));

      per cases ;

        suppose E = {} ;

        hence thesis by A1, A3, A15, Lm2;

      end;

        suppose

         A67: E <> {} ;

        for m be Nat holds (g . m) is_simple_func_in S & (g . m) is nonnegative & (g . m) is E -measurable & E c= ( dom (g . m)) by A15;

        then E common_on_dom g by A67, SEQFUNC:def 9;

        hence thesis by A1, A2, A3, A15, A27, A28, Lm3;

      end;

    end;

    registration

      let X be non empty set;

      cluster additive with_the_same_dom for Functional_Sequence of X, ExtREAL ;

      existence

      proof

        deffunc f( Nat) = <: {} , X, ExtREAL :>;

        consider F be Functional_Sequence of X, ExtREAL such that

         A1: for n be Nat holds (F . n) = f(n) from SEQFUNC:sch 1;

        now

          let n,m be Nat;

          (F . n) = <: {} , X, ExtREAL :> by A1;

          hence ( dom (F . n)) = ( dom (F . m)) by A1;

        end;

        then

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

        take F;

        now

          let n,m be Nat;

          assume n <> m;

          let x be set;

          assume

           A2: x in (( dom (F . n)) /\ ( dom (F . m)));

          (F . n) = <: {} , X, ExtREAL :> by A1;

          then x in (( dom {} ) /\ ( dom (F . m))) by A2, PARTFUN1: 34;

          hence ((F . n) . x) <> +infty or ((F . m) . x) <> -infty ;

        end;

        hence thesis;

      end;

    end

    definition

      let C,D,X be non empty set, F be Function of [:C, D:], ( PFuncs (X, ExtREAL ));

      let c be Element of C, d be Element of D;

      :: original: .

      redefine

      func F . (c,d) -> PartFunc of X, ExtREAL ;

      correctness

      proof

        thus (F . (c,d)) is PartFunc of X, ExtREAL by PARTFUN1: 47;

      end;

    end

    definition

      let C,D,X be non empty set;

      let F be Function of [:C, D:], X;

      let c be Element of C;

      :: MESFUNC9:def6

      func ProjMap1 (F,c) -> Function of D, X means for d be Element of D holds (it . d) = (F . (c,d));

      existence

      proof

        deffunc F( Element of D) = (F . (c,$1));

        consider IT be Function such that

         A1: ( dom IT) = D & for d be Element of D holds (IT . d) = F(d) from FUNCT_1:sch 4;

        now

          let d be object;

          assume

           A2: d in D;

          then

           A3: [c, d] in [:C, D:] by ZFMISC_1: 87;

          (IT . d) = (F . (c,d)) by A1, A2;

          hence (IT . d) in X by A3, FUNCT_2: 5;

        end;

        then

        reconsider IT as Function of D, X by A1, FUNCT_2: 3;

        take IT;

        let d be Element of D;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let P1,P2 be Function of D, X;

        assume that

         A4: for d be Element of D holds (P1 . d) = (F . (c,d)) and

         A5: for d be Element of D holds (P2 . d) = (F . (c,d));

        now

          let d be object;

          assume d in D;

          then

          reconsider d1 = d as Element of D;

          (P1 . d1) = (F . (c,d1)) by A4;

          hence (P1 . d) = (P2 . d) by A5;

        end;

        hence thesis;

      end;

    end

    definition

      let C,D,X be non empty set;

      let F be Function of [:C, D:], X;

      let d be Element of D;

      :: MESFUNC9:def7

      func ProjMap2 (F,d) -> Function of C, X means for c be Element of C holds (it . c) = (F . (c,d));

      existence

      proof

        deffunc F( Element of C) = (F . ($1,d));

        consider IT be Function such that

         A1: ( dom IT) = C & for c be Element of C holds (IT . c) = F(c) from FUNCT_1:sch 4;

        now

          let c be object;

          assume

           A2: c in C;

          then

           A3: [c, d] in [:C, D:] by ZFMISC_1: 87;

          (IT . c) = (F . (c,d)) by A1, A2

          .= (F . [c, d]);

          hence (IT . c) in X by A3, FUNCT_2: 5;

        end;

        then

        reconsider IT as Function of C, X by A1, FUNCT_2: 3;

        take IT;

        let c be Element of C;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let P1,P2 be Function of C, X;

        assume that

         A4: for c be Element of C holds (P1 . c) = (F . (c,d)) and

         A5: for c be Element of C holds (P2 . c) = (F . (c,d));

        now

          let c be object;

          assume c in C;

          then

          reconsider c1 = c as Element of C;

          (P1 . c1) = (F . (c1,d)) by A4;

          hence (P1 . c) = (P2 . c) by A5;

        end;

        hence thesis;

      end;

    end

    definition

      let X,Y be set, F be Function of [: NAT , NAT :], ( PFuncs (X,Y)), n be Nat;

      :: MESFUNC9:def8

      func ProjMap1 (F,n) -> Functional_Sequence of X, Y means

      : Def8: for m be Nat holds (it . m) = (F . (n,m));

      existence

      proof

        deffunc P1( Element of NAT ) = (F . (n,$1));

        consider IT be Function such that

         A1: ( dom IT) = NAT & for m be Element of NAT holds (IT . m) = P1(m) from FUNCT_1:sch 4;

        now

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

          let y be object;

          assume y in ( rng IT);

          then

          consider k be object such that

           A2: k in ( dom IT) and

           A3: y = (IT . k) by FUNCT_1:def 3;

          reconsider k as Element of NAT by A1, A2;

          y = (F . (n1,k)) by A1, A3;

          hence y in ( PFuncs (X,Y));

        end;

        then ( rng IT) c= ( PFuncs (X,Y));

        then

        reconsider IT as Functional_Sequence of X, Y by A1, FUNCT_2:def 1, RELSET_1: 4;

        take IT;

        thus for m be Nat holds (IT . m) = (F . (n,m))

        proof

          let m be Nat;

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

          (IT . m) = (F . (n1,m1)) by A1;

          hence thesis;

        end;

      end;

      uniqueness

      proof

        let G1,G2 be Functional_Sequence of X, Y;

        assume that

         A4: for m be Nat holds (G1 . m) = (F . (n,m)) and

         A5: for m be Nat holds (G2 . m) = (F . (n,m));

        for m be Element of NAT holds (G1 . m) = (G2 . m)

        proof

          let m be Element of NAT ;

          reconsider m1 = m as Nat;

          (G1 . m) = (F . (n,m1)) by A4;

          hence thesis by A5;

        end;

        hence thesis;

      end;

      :: MESFUNC9:def9

      func ProjMap2 (F,n) -> Functional_Sequence of X, Y means

      : Def9: for m be Nat holds (it . m) = (F . (m,n));

      existence

      proof

        deffunc P2( Element of NAT ) = (F . ($1,n));

        consider IT be Function such that

         A6: ( dom IT) = NAT & for m be Element of NAT holds (IT . m) = P2(m) from FUNCT_1:sch 4;

        now

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

          let y be object;

          assume y in ( rng IT);

          then

          consider k be object such that

           A7: k in ( dom IT) and

           A8: y = (IT . k) by FUNCT_1:def 3;

          reconsider k as Element of NAT by A6, A7;

          y = (F . (k,n1)) by A6, A8;

          hence y in ( PFuncs (X,Y));

        end;

        then ( rng IT) c= ( PFuncs (X,Y));

        then

        reconsider IT as Functional_Sequence of X, Y by A6, FUNCT_2:def 1, RELSET_1: 4;

        take IT;

        thus for m be Nat holds (IT . m) = (F . (m,n))

        proof

          let m be Nat;

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

          (IT . m) = (F . (m1,n1)) by A6;

          hence thesis;

        end;

      end;

      uniqueness

      proof

        let G1,G2 be Functional_Sequence of X, Y;

        assume that

         A9: for m be Nat holds (G1 . m) = (F . (m,n)) and

         A10: for m be Nat holds (G2 . m) = (F . (m,n));

        for m be Element of NAT holds (G1 . m) = (G2 . m)

        proof

          let m be Element of NAT ;

          reconsider m1 = m as Nat;

          (G1 . m) = (F . (m1,n)) by A9;

          hence thesis by A10;

        end;

        hence thesis;

      end;

    end

    definition

      let X be non empty set, F be sequence of ( Funcs ( NAT ,( PFuncs (X, ExtREAL )))), n be Nat;

      :: original: .

      redefine

      func F . n -> Functional_Sequence of X, ExtREAL ;

      correctness

      proof

        ex f be Function st (F . n) = f & ( dom f) = NAT & ( rng f) c= ( PFuncs (X, ExtREAL )) by FUNCT_2:def 2;

        hence thesis by FUNCT_2:def 1, RELSET_1: 4;

      end;

    end

    theorem :: MESFUNC9:49

    

     Th49: E = ( dom (F . 0 )) & F is with_the_same_dom & (for n be Nat holds (F . n) is nonnegative & (F . n) is E -measurable) implies ex FF be sequence of ( Funcs ( NAT ,( PFuncs (X, ExtREAL )))) st for n be Nat holds (for m be Nat holds ((FF . n) . m) is_simple_func_in S & ( dom ((FF . n) . m)) = ( dom (F . n))) & (for m be Nat holds ((FF . n) . m) is nonnegative) & (for j,k be Nat st j <= k holds for x be Element of X st x in ( dom (F . n)) holds (((FF . n) . j) . x) <= (((FF . n) . k) . x)) & for x be Element of X st x in ( dom (F . n)) holds ((FF . n) # x) is convergent & ( lim ((FF . n) # x)) = ((F . n) . x)

    proof

      assume that

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

       A2: F is with_the_same_dom and

       A3: for n be Nat holds (F . n) is nonnegative & (F . n) is E -measurable;

      defpred Q[ Element of NAT , set] means for G be Functional_Sequence of X, ExtREAL st $2 = G holds (for m be Nat holds (G . m) is_simple_func_in S & ( dom (G . m)) = ( dom (F . $1))) & (for m be Nat holds (G . m) is nonnegative) & (for j,k be Nat st j <= k holds for x be Element of X st x in ( dom (F . $1)) holds ((G . j) . x) <= ((G . k) . x)) & (for x be Element of X st x in ( dom (F . $1)) holds (G # x) is convergent & ( lim (G # x)) = ((F . $1) . x));

      

       A4: for n be Element of NAT holds ex G be Functional_Sequence of X, ExtREAL st (for m be Nat holds (G . m) is_simple_func_in S & ( dom (G . m)) = ( dom (F . n))) & (for m be Nat holds (G . m) is nonnegative) & (for j,k be Nat st j <= k holds for x be Element of X st x in ( dom (F . n)) holds ((G . j) . x) <= ((G . k) . x)) & for x be Element of X st x in ( dom (F . n)) holds (G # x) is convergent & ( lim (G # x)) = ((F . n) . x)

      proof

        let n be Element of NAT ;

        

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

        

         A6: (F . n) is nonnegative by A3;

        E = ( dom (F . n)) by A1, A2;

        hence thesis by A5, A6, MESFUNC5: 64;

      end;

      

       A7: for n be Element of NAT holds ex G be Element of ( Funcs ( NAT ,( PFuncs (X, ExtREAL )))) st Q[n, G]

      proof

        let n be Element of NAT ;

        consider G be Functional_Sequence of X, ExtREAL such that

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

         A9: for m be Nat holds (G . m) is nonnegative and

         A10: for j,k be Nat st j <= k holds for x be Element of X st x in ( dom (F . n)) holds ((G . j) . x) <= ((G . k) . x) and

         A11: for x be Element of X st x in ( dom (F . n)) holds (G # x) is convergent & ( lim (G # x)) = ((F . n) . x) by A4;

        reconsider G as Element of ( Funcs ( NAT ,( PFuncs (X, ExtREAL )))) by FUNCT_2: 8;

        take G;

        thus thesis by A8, A9, A10, A11;

      end;

      consider FF be sequence of ( Funcs ( NAT ,( PFuncs (X, ExtREAL )))) such that

       A12: for n be Element of NAT holds Q[n, (FF . n)] from FUNCT_2:sch 3( A7);

      take FF;

      thus for n be Nat holds (for m be Nat holds ((FF . n) . m) is_simple_func_in S & ( dom ((FF . n) . m)) = ( dom (F . n))) & (for m be Nat holds ((FF . n) . m) is nonnegative) & (for j,k be Nat st j <= k holds for x be Element of X st x in ( dom (F . n)) holds (((FF . n) . j) . x) <= (((FF . n) . k) . x)) & for x be Element of X st x in ( dom (F . n)) holds ((FF . n) # x) is convergent & ( lim ((FF . n) # x)) = ((F . n) . x)

      proof

        let n be Nat;

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

        for G be Functional_Sequence of X, ExtREAL st (FF . n1) = G holds (for m be Nat holds (G . m) is_simple_func_in S & ( dom (G . m)) = ( dom (F . n1))) & (for m be Nat holds (G . m) is nonnegative) & (for j,k be Nat st j <= k holds for x be Element of X st x in ( dom (F . n1)) holds ((G . j) . x) <= ((G . k) . x)) & for x be Element of X st x in ( dom (F . n1)) holds (G # x) is convergent & ( lim (G # x)) = ((F . n1) . x) by A12;

        hence thesis;

      end;

    end;

    theorem :: MESFUNC9:50

    

     Th50: E = ( dom (F . 0 )) & F is additive & F is with_the_same_dom & (for n be Nat holds (F . n) is E -measurable & (F . n) is nonnegative) implies ex I be ExtREAL_sequence st for n be Nat holds (I . n) = ( Integral (M,(F . n))) & ( Integral (M,(( Partial_Sums F) . n))) = (( Partial_Sums I) . n)

    proof

      assume that

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

       A2: F is additive and

       A3: F is with_the_same_dom and

       A4: for n be Nat holds (F . n) is E -measurable & (F . n) is nonnegative;

      set PF = ( Partial_Sums F);

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

      consider I be sequence of ExtREAL such that

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

      reconsider I as ExtREAL_sequence;

      take I;

      

       A6: for n be Nat holds (F . n) is without-infty by A4, MESFUNC5: 12;

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

      proof

        set PI = ( Partial_Sums I);

        defpred P2[ Nat] means ( Integral (M,(PF . $1))) = (( Partial_Sums I) . $1);

        let n be Nat;

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

        (I . n) = ( Integral (M,(F . n9))) by A5;

        hence (I . n) = ( Integral (M,(F . n)));

        

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

        proof

          let k be Nat;

          assume

           A8: P2[k];

          

           A9: (F . (k + 1)) is E -measurable by A4;

          

           A10: ( dom (F . (k + 1))) = E by A1, A3;

          

           A11: (PF . (k + 1)) is E -measurable by A4, A6, Th41;

          

           A12: (F . (k + 1)) is nonnegative by A4;

          

           A13: (PF . k) is nonnegative by A4, Th36;

          

           A14: ( dom (PF . k)) = E by A1, A2, A3, Th29;

          

           A15: (PF . k) is E -measurable by A4, A6, Th41;

          then

          consider D be Element of S such that

           A16: D = ( dom ((PF . k) + (F . (k + 1)))) and

           A17: ( integral+ (M,((PF . k) + (F . (k + 1))))) = (( integral+ (M,((PF . k) | D))) + ( integral+ (M,((F . (k + 1)) | D)))) by A14, A10, A9, A13, A12, MESFUNC5: 78;

          

           A18: D = (( dom (PF . k)) /\ ( dom (F . (k + 1)))) by A13, A12, A16, MESFUNC5: 22

          .= E by A14, A10;

          then

           A19: ((PF . k) | D) = (PF . k) by A14;

          

           A20: ((F . (k + 1)) | D) = (F . (k + 1)) by A10, A18;

          ( dom (PF . (k + 1))) = E by A1, A2, A3, Th29;

          

          then ( Integral (M,(PF . (k + 1)))) = ( integral+ (M,(PF . (k + 1)))) by A4, A11, Th36, MESFUNC5: 88

          .= (( integral+ (M,((PF . k) | D))) + ( integral+ (M,((F . (k + 1)) | D)))) by A17, Def4

          .= (( Integral (M,(PF . k))) + ( integral+ (M,((F . (k + 1)) | D)))) by A14, A15, A13, A19, MESFUNC5: 88

          .= (( Integral (M,(PF . k))) + ( Integral (M,(F . (k + 1))))) by A10, A9, A12, A20, MESFUNC5: 88

          .= ((PI . k) + (I . (k + 1))) by A5, A8;

          hence thesis by Def1;

        end;

        ( Integral (M,(PF . 0 ))) = ( Integral (M,(F . 0 ))) by Def4;

        then ( Integral (M,(PF . 0 ))) = (I . 0 ) by A5;

        then

         A21: P2[ 0 ] by Def1;

        for k be Nat holds P2[k] from NAT_1:sch 2( A21, A7);

        hence thesis;

      end;

    end;

    

     Lm4: E = ( dom (F . 0 )) & F is additive & F is with_the_same_dom & (for n be Nat holds (F . n) is nonnegative & (F . n) is E -measurable) & (for x be Element of X st x in E holds (F # x) is summable) implies ex I be ExtREAL_sequence st (for n be Nat holds (I . n) = ( Integral (M,((F . n) | E)))) & I is summable & ( Integral (M,(( lim ( Partial_Sums F)) | E))) = ( Sum I)

    proof

      assume that

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

       A2: F is additive and

       A3: F is with_the_same_dom and

       A4: for n be Nat holds (F . n) is nonnegative & (F . n) is E -measurable and

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

      consider FF be sequence of ( Funcs ( NAT ,( PFuncs (X, ExtREAL )))) such that

       A6: for n be Nat holds (for m be Nat holds ((FF . n) . m) is_simple_func_in S & ( dom ((FF . n) . m)) = ( dom (F . n))) & (for m be Nat holds ((FF . n) . m) is nonnegative) & (for j,k be Nat st j <= k holds for x be Element of X st x in ( dom (F . n)) holds (((FF . n) . j) . x) <= (((FF . n) . k) . x)) & for x be Element of X st x in ( dom (F . n)) holds ((FF . n) # x) is convergent & ( lim ((FF . n) # x)) = ((F . n) . x) by A1, A3, A4, Th49;

      defpred PP[ Element of NAT , Element of NAT , set] means for n,m be Nat st n = $1 & m = $2 holds $3 = ((FF . n) . m);

      

       A7: for i1 be Element of NAT holds for j1 be Element of NAT holds ex F1 be Element of ( PFuncs (X, ExtREAL )) st PP[i1, j1, F1]

      proof

        let i1 be Element of NAT ;

        let j1 be Element of NAT ;

        reconsider i = i1, j = j1 as Nat;

        reconsider F1 = ((FF . i) . j) as Element of ( PFuncs (X, ExtREAL )) by PARTFUN1: 45;

        take F1;

        thus thesis;

      end;

      consider FF2 be Function of [: NAT , NAT :], ( PFuncs (X, ExtREAL )) such that

       A8: for i be Element of NAT holds for j be Element of NAT holds PP[i, j, (FF2 . (i,j))] from BINOP_1:sch 3( A7);

      deffunc Phi( Nat) = (( Partial_Sums ( ProjMap2 (FF2,$1))) . $1);

      consider P be Functional_Sequence of X, ExtREAL such that

       A9: for k be Nat holds (P . k) = Phi(k) from SEQFUNC:sch 1;

      

       A10: for n be Nat holds (for m be Nat holds ( dom (( ProjMap1 (FF2,n)) . m)) = E & ( dom (( ProjMap2 (FF2,n)) . m)) = E & (( ProjMap1 (FF2,n)) . m) is_simple_func_in S & (( ProjMap2 (FF2,n)) . m) is_simple_func_in S) & ( ProjMap1 (FF2,n)) is additive & ( ProjMap2 (FF2,n)) is additive & ( ProjMap1 (FF2,n)) is with_the_same_dom & ( ProjMap2 (FF2,n)) is with_the_same_dom

      proof

        let n be Nat;

         A11:

        now

          let m be Nat;

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

          

           A12: (( ProjMap1 (FF2,n)) . m) = (FF2 . (n,m)) by Def8;

          

           A13: (FF2 . (n1,m1)) = ((FF . n1) . m) by A8;

          

           A14: ( dom (F . m1)) = ( dom (F . 0 )) by A3;

          

           A15: (( ProjMap2 (FF2,n)) . m) = (FF2 . (m,n)) by Def9;

          

           A16: (FF2 . (m1,n1)) = ((FF . m1) . n) by A8;

          ( dom (F . n1)) = ( dom (F . m1)) by A3;

          hence ( dom (( ProjMap1 (FF2,n)) . m)) = E & ( dom (( ProjMap2 (FF2,n)) . m)) = E by A1, A6, A12, A15, A13, A16, A14;

          thus (( ProjMap1 (FF2,n)) . m) is_simple_func_in S & (( ProjMap2 (FF2,n)) . m) is_simple_func_in S by A6, A12, A15, A13, A16;

        end;

        for i1,j1 be Nat holds ( dom (( ProjMap1 (FF2,n)) . i1)) = ( dom (( ProjMap1 (FF2,n)) . j1)) & ( dom (( ProjMap2 (FF2,n)) . i1)) = ( dom (( ProjMap2 (FF2,n)) . j1))

        proof

          let i1,j1 be Nat;

          

           A17: ( dom (( ProjMap2 (FF2,n)) . i1)) = E by A11;

          ( dom (( ProjMap1 (FF2,n)) . i1)) = E by A11;

          hence thesis by A11, A17;

        end;

        hence thesis by A11, Th35;

      end;

      for n,m be Nat holds ( dom (P . n)) = ( dom (P . m))

      proof

        let n,m be Nat;

        

         A18: ( ProjMap2 (FF2,n)) is with_the_same_dom by A10;

        

         A19: ( dom (P . n)) = ( dom (( Partial_Sums ( ProjMap2 (FF2,n))) . n)) by A9;

        ( ProjMap2 (FF2,n)) is additive by A10;

        then ( dom (P . n)) = ( dom (( ProjMap2 (FF2,n)) . 0 )) by A18, A19, Th29;

        then ( dom (P . n)) = E by A10;

        then

         A20: ( dom (P . n)) = ( dom (( ProjMap2 (FF2,m)) . 0 )) by A10;

        

         A21: ( ProjMap2 (FF2,m)) is with_the_same_dom by A10;

        ( ProjMap2 (FF2,m)) is additive by A10;

        then ( dom (P . n)) = ( dom (( Partial_Sums ( ProjMap2 (FF2,m))) . m)) by A21, A20, Th29;

        hence thesis by A9;

      end;

      then

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

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

      then ( dom ( lim P)) = ( dom (( Partial_Sums ( ProjMap2 (FF2, 0 ))) . 0 )) by A9;

      then ( dom ( lim P)) = ( dom (( ProjMap2 (FF2, 0 )) . 0 )) by Def4;

      then ( dom ( lim P)) = ( dom (FF2 . ( 0 , 0 ))) by Def9;

      then

       A22: ( dom ( lim P)) = ( dom ((FF . 0 ) . 0 )) by A8;

      then

       A23: ( dom ( lim P)) = ( dom (F . 0 )) by A6;

      

       A24: for k be Nat holds for m be Nat, x be Element of X st x in (( dom (F . 0 )) /\ ( dom (( ProjMap2 (FF2,k)) . 0 ))) holds ((( ProjMap2 (FF2,k)) . m) . x) <= ((F . m) . x)

      proof

        let k be Nat;

        let m be Nat, x be Element of X;

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

        assume x in (( dom (F . 0 )) /\ ( dom (( ProjMap2 (FF2,k)) . 0 )));

        then x in ( dom (F . 0 )) by XBOOLE_0:def 4;

        then

         A25: x in ( dom (F . m)) by A3;

        ((FF . m1) # x) is non-decreasing

        proof

          let j,k be ExtReal;

          assume that

           A26: j in ( dom ((FF . m1) # x)) and

           A27: k in ( dom ((FF . m1) # x)) and

           A28: j <= k;

          reconsider j, k as Element of NAT by A26, A27;

          

           A29: (((FF . m1) # x) . k) = (((FF . m1) . k) . x) by MESFUNC5:def 13;

          (((FF . m1) # x) . j) = (((FF . m1) . j) . x) by MESFUNC5:def 13;

          hence thesis by A6, A25, A28, A29;

        end;

        then ( lim ((FF . m1) # x)) = ( sup ((FF . m1) # x)) by RINFSUP2: 37;

        then (((FF . m1) # x) . k1) <= ( lim ((FF . m1) # x)) by RINFSUP2: 23;

        then

         A30: (((FF . m1) # x) . k) <= ((F . m1) . x) by A6, A25;

        (( ProjMap2 (FF2,k)) . m) = (FF2 . (m1,k1)) by Def9;

        then (( ProjMap2 (FF2,k)) . m) = ((FF . m) . k) by A8;

        hence thesis by A30, MESFUNC5:def 13;

      end;

      

       A31: for x be Element of X, k be Element of NAT st x in ( dom ( lim P)) holds ((P # x) . k) <= ((( Partial_Sums F) # x) . k)

      proof

        let x be Element of X;

        let k be Element of NAT ;

        assume

         A32: x in ( dom ( lim P));

        ( dom (( ProjMap2 (FF2,k)) . 0 )) = E by A10;

        then

         A33: x in (( dom (F . 0 )) /\ ( dom (( ProjMap2 (FF2,k)) . 0 ))) by A1, A6, A22, A32;

        

         A34: ( ProjMap2 (FF2,k)) is with_the_same_dom by A10;

        ((P # x) . k) = ((P . k) . x) by MESFUNC5:def 13;

        then

         A35: ((P # x) . k) = ((( Partial_Sums ( ProjMap2 (FF2,k))) . k) . x) by A9;

        

         A36: for m be Nat, x be Element of X st x in (( dom (F . 0 )) /\ ( dom (( ProjMap2 (FF2,k)) . 0 ))) holds ((( ProjMap2 (FF2,k)) . m) . x) <= ((F . m) . x) by A24;

        ( ProjMap2 (FF2,k)) is additive by A10;

        then ((( Partial_Sums ( ProjMap2 (FF2,k))) . k) . x) <= ((( Partial_Sums F) . k) . x) by A2, A3, A33, A34, A36, Th42;

        hence thesis by A35, MESFUNC5:def 13;

      end;

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

      then

       A37: ( dom ( lim ( Partial_Sums F))) = E by A1, Def4;

      

       A38: for n,m be Nat holds (( ProjMap1 (FF2,n)) . m) is nonnegative & (( ProjMap2 (FF2,n)) . m) is nonnegative

      proof

        let n,m be Nat;

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

        (( ProjMap1 (FF2,n)) . m) = (FF2 . (n1,m1)) by Def8;

        then (( ProjMap1 (FF2,n)) . m) = ((FF . n) . m) by A8;

        hence (( ProjMap1 (FF2,n)) . m) is nonnegative by A6;

        (( ProjMap2 (FF2,n)) . m) = (FF2 . (m1,n1)) by Def9;

        then (( ProjMap2 (FF2,n)) . m) = ((FF . m) . n) by A8;

        hence thesis by A6;

      end;

      

       A39: for n be Element of NAT holds for x be Element of X st x in E holds (( ProjMap1 (FF2,n)) # x) is convergent & ((F . n) . x) = ( lim (( ProjMap1 (FF2,n)) # x))

      proof

        let n be Element of NAT ;

        reconsider n1 = n as Nat;

        let x be Element of X;

        assume

         A40: x in E;

        for k be Nat holds ex m be Nat st k <= m & ((( ProjMap1 (FF2,n)) # x) . m) > ( - 1)

        proof

          let k be Nat;

          take m = k;

          

           A41: ((( ProjMap1 (FF2,n)) # x) . m) = ((( ProjMap1 (FF2,n)) . m) . x) by MESFUNC5:def 13;

          (( ProjMap1 (FF2,n)) . m) is nonnegative by A38;

          hence thesis by A41, SUPINF_2: 39;

        end;

        then

         A42: not (( ProjMap1 (FF2,n)) # x) is convergent_to_-infty;

        

         A43: E = ( dom (F . n1)) by A1, A3;

        (( ProjMap1 (FF2,n)) # x) is non-decreasing

        proof

          let i,j be ExtReal;

          assume that

           A44: i in ( dom (( ProjMap1 (FF2,n)) # x)) and

           A45: j in ( dom (( ProjMap1 (FF2,n)) # x)) and

           A46: i <= j;

          reconsider i1 = i, j1 = j as Element of NAT by A44, A45;

          

           A47: ((( ProjMap1 (FF2,n)) # x) . i1) = ((( ProjMap1 (FF2,n)) . i1) . x) by MESFUNC5:def 13;

          (( ProjMap1 (FF2,n)) . i1) = (FF2 . (n,i1)) by Def8;

          then

           A48: (( ProjMap1 (FF2,n)) . i1) = ((FF . n1) . i1) by A8;

          

           A49: ((( ProjMap1 (FF2,n)) # x) . j1) = ((( ProjMap1 (FF2,n)) . j1) . x) by MESFUNC5:def 13;

          

           A50: (( ProjMap1 (FF2,n)) . j1) = (FF2 . (n,j1)) by Def8;

          (((FF . n1) . i1) . x) <= (((FF . n1) . j1) . x) by A6, A43, A40, A46;

          hence thesis by A8, A47, A49, A48, A50;

        end;

        hence

         A51: (( ProjMap1 (FF2,n)) # x) is convergent by RINFSUP2: 37;

        per cases by A51, A42;

          suppose

           A52: (( ProjMap1 (FF2,n)) # x) is convergent_to_finite_number;

          then

           A53: not (( ProjMap1 (FF2,n)) # x) is convergent_to_-infty by MESFUNC5: 51;

           not (( ProjMap1 (FF2,n)) # x) is convergent_to_+infty by A52, MESFUNC5: 50;

          then

          consider lP be Real such that

           A54: ( lim (( ProjMap1 (FF2,n)) # x)) = lP and

           A55: for p be Real st 0 < p holds ex nn be Nat st for mm be Nat st nn <= mm holds |.(((( ProjMap1 (FF2,n)) # x) . mm) - ( lim (( ProjMap1 (FF2,n)) # x))).| < p and (( ProjMap1 (FF2,n)) # x) is convergent_to_finite_number by A51, A53, MESFUNC5:def 12;

          

           A56: for p be Real st 0 < p holds ex nn be Nat st for mm be Nat st nn <= mm holds |.((((FF . n1) # x) . mm) - lP).| < p

          proof

            let p be Real;

            assume 0 < p;

            then

            consider nn be Nat such that

             A57: for mm be Nat st nn <= mm holds |.(((( ProjMap1 (FF2,n)) # x) . mm) - ( lim (( ProjMap1 (FF2,n)) # x))).| < p by A55;

            take nn;

            let mm be Nat;

            assume

             A58: nn <= mm;

            reconsider mm1 = mm as Element of NAT by ORDINAL1:def 12;

            (( ProjMap1 (FF2,n)) . mm) = (FF2 . (n,mm)) by Def8;

            then

             A59: (( ProjMap1 (FF2,n)) . mm) = ((FF . n1) . mm1) by A8;

            ((( ProjMap1 (FF2,n)) # x) . mm) = ((( ProjMap1 (FF2,n)) . mm) . x) by MESFUNC5:def 13;

            then (((FF . n1) # x) . mm) = ((( ProjMap1 (FF2,n)) # x) . mm) by A59, MESFUNC5:def 13;

            hence thesis by A54, A57, A58;

          end;

          then

           A60: ((FF . n1) # x) is convergent_to_finite_number;

          reconsider lP as R_eal by XXREAL_0:def 1;

          ((FF . n1) # x) is convergent by A60;

          then ( lim ((FF . n1) # x)) = lP by A56, A60, MESFUNC5:def 12;

          hence thesis by A6, A43, A40, A54;

        end;

          suppose

           A61: (( ProjMap1 (FF2,n)) # x) is convergent_to_+infty;

          for g be Real st 0 < g holds ex nn be Nat st for mm be Nat st nn <= mm holds g <= (((FF . n1) # x) . mm)

          proof

            let g be Real;

            assume 0 < g;

            then

            consider nn be Nat such that

             A62: for mm be Nat st nn <= mm holds g <= ((( ProjMap1 (FF2,n)) # x) . mm) by A61;

            take nn;

            let mm be Nat;

            assume nn <= mm;

            then

             A63: g <= ((( ProjMap1 (FF2,n)) # x) . mm) by A62;

            reconsider mm1 = mm as Element of NAT by ORDINAL1:def 12;

            (( ProjMap1 (FF2,n)) . mm) = (FF2 . (n,mm1)) by Def8;

            then

             A64: (( ProjMap1 (FF2,n)) . mm) = ((FF . n) . mm) by A8;

            ((( ProjMap1 (FF2,n)) # x) . mm) = ((( ProjMap1 (FF2,n)) . mm) . x) by MESFUNC5:def 13;

            hence thesis by A63, A64, MESFUNC5:def 13;

          end;

          then

           A65: ((FF . n1) # x) is convergent_to_+infty;

          then ((FF . n1) # x) is convergent;

          then

           A66: ( lim ((FF . n1) # x)) = +infty by A65, MESFUNC5:def 12;

          ( lim (( ProjMap1 (FF2,n)) # x)) = +infty by A51, A61, MESFUNC5:def 12;

          hence thesis by A6, A43, A40, A66;

        end;

      end;

      

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

      then

       A68: ( dom ( lim ( Partial_Sums F))) = E by A1, Def4;

      

       A69: for n be Nat holds ( dom (P . n)) = ( dom ( lim ( Partial_Sums F)))

      proof

        let n be Nat;

        

         A70: ( ProjMap2 (FF2,n)) is with_the_same_dom by A10;

        

         A71: ( dom (P . n)) = ( dom (( Partial_Sums ( ProjMap2 (FF2,n))) . n)) by A9;

        ( ProjMap2 (FF2,n)) is additive by A10;

        then ( dom (P . n)) = ( dom (( ProjMap2 (FF2,n)) . 0 )) by A70, A71, Th29;

        hence thesis by A68, A10;

      end;

      

       A72: for n,m be Nat st n <= m holds for i be Nat, x be Element of X st x in E holds ((( ProjMap2 (FF2,n)) . i) . x) <= ((( ProjMap2 (FF2,m)) . i) . x)

      proof

        let n,m be Nat;

        assume

         A73: n <= m;

        let i be Nat, x be Element of X;

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

        ((( ProjMap2 (FF2,n)) . i) . x) = ((FF2 . (i1,n1)) . x) by Def9;

        then

         A74: ((( ProjMap2 (FF2,n)) . i) . x) = (((FF . i) . n) . x) by A8;

        ((( ProjMap2 (FF2,m)) . i) . x) = ((FF2 . (i1,m1)) . x) by Def9;

        then

         A75: ((( ProjMap2 (FF2,m)) . i) . x) = (((FF . i) . m) . x) by A8;

        assume x in E;

        then x in ( dom (F . i)) by A1, A3;

        hence thesis by A6, A73, A74, A75;

      end;

      

       A76: for n,m be Nat st n <= m holds for i be Nat, x be Element of X st x in E holds ((( Partial_Sums ( ProjMap2 (FF2,n))) . i) . x) <= ((( Partial_Sums ( ProjMap2 (FF2,m))) . i) . x)

      proof

        let n,m be Nat;

        

         A77: ( ProjMap2 (FF2,n)) is with_the_same_dom by A10;

        

         A78: ( ProjMap2 (FF2,m)) is additive by A10;

        assume

         A79: n <= m;

        

         A80: for i be Nat, x be Element of X st x in (( dom (( ProjMap2 (FF2,n)) . 0 )) /\ ( dom (( ProjMap2 (FF2,m)) . 0 ))) holds ((( ProjMap2 (FF2,n)) . i) . x) <= ((( ProjMap2 (FF2,m)) . i) . x)

        proof

          let i be Nat, x be Element of X;

          assume x in (( dom (( ProjMap2 (FF2,n)) . 0 )) /\ ( dom (( ProjMap2 (FF2,m)) . 0 )));

          then x in ( dom (( ProjMap2 (FF2,n)) . 0 )) by XBOOLE_0:def 4;

          then x in E by A10;

          hence thesis by A72, A79;

        end;

        let i be Nat, x be Element of X;

        assume

         A81: x in E;

        then

         A82: x in ( dom (( ProjMap2 (FF2,m)) . 0 )) by A10;

        x in ( dom (( ProjMap2 (FF2,n)) . 0 )) by A10, A81;

        then

         A83: x in (( dom (( ProjMap2 (FF2,n)) . 0 )) /\ ( dom (( ProjMap2 (FF2,m)) . 0 ))) by A82, XBOOLE_0:def 4;

        

         A84: ( ProjMap2 (FF2,m)) is with_the_same_dom by A10;

        ( ProjMap2 (FF2,n)) is additive by A10;

        hence thesis by A83, A77, A78, A84, A80, Th42;

      end;

      

       A85: for n,m be Nat st n <= m holds for x be Element of X st x in E holds ((P . n) . x) <= ((P . m) . x)

      proof

        let n,m be Nat;

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

        assume

         A86: n <= m;

        let x be Element of X;

        

         A87: ( ProjMap2 (FF2,m)) is with_the_same_dom by A10;

        

         A88: for n be Nat holds (( ProjMap2 (FF2,m)) . n) is nonnegative by A38;

        assume

         A89: x in E;

        then x in ( dom (( ProjMap2 (FF2,m)) . 0 )) by A10;

        then (( Partial_Sums ( ProjMap2 (FF2,m))) # x) is non-decreasing by A87, A88, Th38;

        then ((( Partial_Sums ( ProjMap2 (FF2,m))) # x) . n1) <= ((( Partial_Sums ( ProjMap2 (FF2,m))) # x) . m1) by A86, RINFSUP2: 7;

        then ((( Partial_Sums ( ProjMap2 (FF2,m))) . n) . x) <= ((( Partial_Sums ( ProjMap2 (FF2,m))) # x) . m1) by MESFUNC5:def 13;

        then ((( Partial_Sums ( ProjMap2 (FF2,m))) . n) . x) <= ((( Partial_Sums ( ProjMap2 (FF2,m))) . m) . x) by MESFUNC5:def 13;

        then

         A90: ((( Partial_Sums ( ProjMap2 (FF2,m))) . n) . x) <= ((P . m) . x) by A9;

        ((( Partial_Sums ( ProjMap2 (FF2,n))) . n) . x) <= ((( Partial_Sums ( ProjMap2 (FF2,m))) . n) . x) by A76, A86, A89;

        then ((P . n) . x) <= ((( Partial_Sums ( ProjMap2 (FF2,m))) . n) . x) by A9;

        hence thesis by A90, XXREAL_0: 2;

      end;

      

       A91: for x be Element of X st x in ( dom ( lim P)) holds (P # x) is convergent

      proof

        let x be Element of X;

        assume

         A92: x in ( dom ( lim P));

        for n,m be Nat st m <= n holds ((P # x) . m) <= ((P # x) . n)

        proof

          let n,m be Nat;

          assume m <= n;

          then ((P . m) . x) <= ((P . n) . x) by A1, A85, A23, A92;

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

          hence thesis by MESFUNC5:def 13;

        end;

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

        hence thesis by RINFSUP2: 37;

      end;

      

       A93: for x be Element of X st x in ( dom ( lim P)) holds ( lim (P # x)) = ( lim (( Partial_Sums F) # x))

      proof

        defpred PP2[ Element of NAT , Element of NAT , set] means for n,m be Nat st n = $1 & m = $2 holds $3 = (( Partial_Sums ( ProjMap2 (FF2,n))) . m);

        let x be Element of X;

        

         A94: for i1 be Element of NAT holds for j1 be Element of NAT holds ex PP2 be Element of ( PFuncs (X, ExtREAL )) st PP2[i1, j1, PP2]

        proof

          let i1 be Element of NAT ;

          let j1 be Element of NAT ;

          reconsider i = i1, j = j1 as Nat;

          reconsider F1 = (( Partial_Sums ( ProjMap2 (FF2,i))) . j) as Element of ( PFuncs (X, ExtREAL )) by PARTFUN1: 45;

          take F1;

          thus thesis;

        end;

        consider PP2 be Function of [: NAT , NAT :], ( PFuncs (X, ExtREAL )) such that

         A95: for i be Element of NAT holds for j be Element of NAT holds PP2[i, j, (PP2 . (i,j))] from BINOP_1:sch 3( A94);

        assume

         A96: x in ( dom ( lim P));

        then

         A97: (P # x) is convergent by A91;

        

         A98: for p,n be Element of NAT holds (( ProjMap2 (PP2,n)) . p) = (( Partial_Sums ( ProjMap2 (FF2,p))) . n)

        proof

          let p,n be Element of NAT ;

          (( ProjMap2 (PP2,n)) . p) = (PP2 . (p,n)) by Def9;

          hence thesis by A95;

        end;

        

         A99: for n be Element of NAT holds (( ProjMap2 (PP2,n)) # x) is convergent & ((( ProjMap2 (PP2,n)) # x) ^\ n) is convergent & ( lim (( ProjMap2 (PP2,n)) # x)) = ( lim ((( ProjMap2 (PP2,n)) # x) ^\ n))

        proof

          let n be Element of NAT ;

          (( ProjMap2 (PP2,n)) # x) is non-decreasing

          proof

            let j,k be ExtReal;

            assume that

             A100: j in ( dom (( ProjMap2 (PP2,n)) # x)) and

             A101: k in ( dom (( ProjMap2 (PP2,n)) # x)) and

             A102: j <= k;

            reconsider j, k as Element of NAT by A100, A101;

            

             A103: ( ProjMap2 (FF2,j)) is additive by A10;

            

             A104: ( ProjMap2 (FF2,k)) is with_the_same_dom by A10;

            

             A105: ( dom (( ProjMap2 (FF2,k)) . 0 )) = E by A10;

            ((( ProjMap2 (PP2,n)) # x) . k) = ((( ProjMap2 (PP2,n)) . k) . x) by MESFUNC5:def 13;

            then

             A106: ((( ProjMap2 (PP2,n)) # x) . k) = ((( Partial_Sums ( ProjMap2 (FF2,k))) . n) . x) by A98;

            

             A107: ( ProjMap2 (FF2,k)) is additive by A10;

            ((( ProjMap2 (PP2,n)) # x) . j) = ((( ProjMap2 (PP2,n)) . j) . x) by MESFUNC5:def 13;

            then

             A108: ((( ProjMap2 (PP2,n)) # x) . j) = ((( Partial_Sums ( ProjMap2 (FF2,j))) . n) . x) by A98;

            

             A109: ( ProjMap2 (FF2,j)) is with_the_same_dom by A10;

            

             A110: ( dom (( ProjMap2 (FF2,j)) . 0 )) = E by A10;

            then for i be Nat, z be Element of X st z in (( dom (( ProjMap2 (FF2,j)) . 0 )) /\ ( dom (( ProjMap2 (FF2,k)) . 0 ))) holds ((( ProjMap2 (FF2,j)) . i) . z) <= ((( ProjMap2 (FF2,k)) . i) . z) by A72, A102, A105;

            hence thesis by A1, A23, A96, A108, A106, A103, A109, A107, A104, A110, A105, Th42;

          end;

          hence (( ProjMap2 (PP2,n)) # x) is convergent by RINFSUP2: 37;

          hence thesis by RINFSUP2: 21;

        end;

        

         A111: for n be Nat holds ((( Partial_Sums F) # x) . n) <= ( lim (P # x))

        proof

          for p be object st p in NAT holds ((( ProjMap2 (PP2, 0 )) # x) . p) = ((( ProjMap1 (FF2, 0 )) # x) . p)

          proof

            let p be object;

            assume p in NAT ;

            then

            reconsider p9 = p as Element of NAT ;

            (( ProjMap2 (PP2, 0 )) . p9) = (( Partial_Sums ( ProjMap2 (FF2,p9))) . 0 ) by A98;

            then (( ProjMap2 (PP2, 0 )) . p9) = (( ProjMap2 (FF2,p9)) . 0 ) by Def4;

            then (( ProjMap2 (PP2, 0 )) . p9) = (FF2 . ( 0 ,p9)) by Def9;

            then

             A112: (( ProjMap2 (PP2, 0 )) . p9) = (( ProjMap1 (FF2, 0 )) . p9) by Def8;

            ((( ProjMap2 (PP2, 0 )) # x) . p) = ((( ProjMap2 (PP2, 0 )) . p9) . x) by MESFUNC5:def 13;

            hence thesis by A112, MESFUNC5:def 13;

          end;

          then (( ProjMap2 (PP2, 0 )) # x) = (( ProjMap1 (FF2, 0 )) # x);

          then

           A113: ( lim (( ProjMap2 (PP2, 0 )) # x)) = ((F . 0 ) . x) by A1, A39, A23, A96;

          defpred C[ Nat] means ( lim (( ProjMap2 (PP2,$1)) # x)) = ((( Partial_Sums F) # x) . $1);

          let n be Nat;

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

          

           A114: ( lim ((P # x) ^\ n9)) = ( lim (P # x)) by A97, RINFSUP2: 21;

          

           A115: ((( ProjMap2 (PP2,n)) # x) ^\ n9) is convergent by A99;

          

           A116: for k be Nat st C[k] holds C[(k + 1)]

          proof

            let k be Nat;

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

            assume

             A117: C[k];

            

             A118: (( ProjMap2 (PP2,k9)) # x) is convergent by A99;

            now

              let m be object;

              assume m in ( dom (( ProjMap1 (FF2,(k + 1))) # x));

              then

              reconsider m1 = m as Element of NAT ;

              (( ProjMap1 (FF2,(k + 1))) . m1) is nonnegative by A38;

              then 0. <= ((( ProjMap1 (FF2,(k + 1))) . m1) . x) by SUPINF_2: 51;

              hence 0. <= ((( ProjMap1 (FF2,(k + 1))) # x) . m) by MESFUNC5:def 13;

            end;

            then

             A119: (( ProjMap1 (FF2,(k + 1))) # x) is nonnegative by SUPINF_2: 52;

            now

              let m be object;

              assume m in ( dom (( ProjMap2 (PP2,k)) # x));

              then

              reconsider m1 = m as Element of NAT ;

              

               A120: (( ProjMap2 (PP2,k)) . m1) = (( Partial_Sums ( ProjMap2 (FF2,m1))) . k9) by A98;

              for l be Nat holds (( ProjMap2 (FF2,m1)) . l) is nonnegative by A38;

              then (( ProjMap2 (PP2,k)) . m1) is nonnegative by A120, Th36;

              then 0. <= ((( ProjMap2 (PP2,k)) . m1) . x) by SUPINF_2: 51;

              hence 0. <= ((( ProjMap2 (PP2,k)) # x) . m) by MESFUNC5:def 13;

            end;

            then

             A121: (( ProjMap2 (PP2,k)) # x) is nonnegative by SUPINF_2: 52;

            x in ( dom (( Partial_Sums F) . (k + 1))) by A2, A3, A23, A96, Th29;

            then

             A122: x in ( dom ((( Partial_Sums F) . k) + (F . (k + 1)))) by Def4;

            

             A123: for p be Nat holds ((( ProjMap2 (PP2,(k + 1))) # x) . p) = (((( ProjMap2 (PP2,k)) # x) . p) + ((( ProjMap1 (FF2,(k + 1))) # x) . p))

            proof

              let p be Nat;

              reconsider p9 = p as Element of NAT by ORDINAL1:def 12;

              

               A124: (( ProjMap2 (FF2,p9)) . (k + 1)) = (FF2 . ((k + 1),p9)) by Def9;

              

               A125: ( ProjMap2 (FF2,p)) is with_the_same_dom by A10;

              

               A126: ( dom (( ProjMap2 (FF2,p)) . 0 )) = E by A10;

              ( ProjMap2 (FF2,p)) is additive by A10;

              then E c= ( dom (( Partial_Sums ( ProjMap2 (FF2,p))) . (k + 1))) by A125, A126, Th29;

              then

               A127: E c= ( dom (( ProjMap2 (PP2,(k + 1))) . p9)) by A98;

              (( ProjMap2 (PP2,(k + 1))) . p9) = (( Partial_Sums ( ProjMap2 (FF2,p9))) . (k + 1)) by A98;

              then

               A128: (( ProjMap2 (PP2,(k + 1))) . p9) = ((( Partial_Sums ( ProjMap2 (FF2,p9))) . k) + (( ProjMap2 (FF2,p9)) . (k + 1))) by Def4;

              (( Partial_Sums ( ProjMap2 (FF2,p9))) . k9) = (( ProjMap2 (PP2,k)) . p9) by A98;

              then (( ProjMap2 (PP2,(k + 1))) . p9) = ((( ProjMap2 (PP2,k)) . p9) + (( ProjMap1 (FF2,(k + 1))) . p9)) by A128, A124, Def8;

              then ((( ProjMap2 (PP2,(k + 1))) . p9) . x) = (((( ProjMap2 (PP2,k)) . p9) . x) + ((( ProjMap1 (FF2,(k + 1))) . p9) . x)) by A1, A23, A96, A127, MESFUNC1:def 3;

              then

               A129: ((( ProjMap2 (PP2,(k + 1))) . p9) . x) = (((( ProjMap2 (PP2,k)) # x) . p) + ((( ProjMap1 (FF2,(k + 1))) . p9) . x)) by MESFUNC5:def 13;

              ((( ProjMap2 (PP2,(k + 1))) # x) . p) = ((( ProjMap2 (PP2,(k + 1))) . p9) . x) by MESFUNC5:def 13;

              hence thesis by A129, MESFUNC5:def 13;

            end;

            

             A130: ( lim (( ProjMap1 (FF2,(k + 1))) # x)) = ((F . (k + 1)) . x) by A1, A39, A23, A96;

            (( ProjMap1 (FF2,(k + 1))) # x) is convergent by A1, A39, A23, A96;

            then ( lim (( ProjMap2 (PP2,(k + 1))) # x)) = (( lim (( ProjMap2 (PP2,k)) # x)) + ( lim (( ProjMap1 (FF2,(k + 1))) # x))) by A118, A121, A119, A123, Th11;

            then ( lim (( ProjMap2 (PP2,(k + 1))) # x)) = (((( Partial_Sums F) . k) . x) + ((F . (k + 1)) . x)) by A117, A130, MESFUNC5:def 13;

            then ( lim (( ProjMap2 (PP2,(k + 1))) # x)) = (((( Partial_Sums F) . k) + (F . (k + 1))) . x) by A122, MESFUNC1:def 3;

            then ( lim (( ProjMap2 (PP2,(k + 1))) # x)) = ((( Partial_Sums F) . (k + 1)) . x) by Def4;

            hence thesis by MESFUNC5:def 13;

          end;

          

           A131: for p be Nat holds (((( ProjMap2 (PP2,n)) # x) ^\ n9) . p) <= (((P # x) ^\ n9) . p)

          proof

            let p be Nat;

            

             A132: (n + p) in NAT by ORDINAL1:def 12;

            

             A133: n <= (n + p) by NAT_1: 11;

            

             A134: ( ProjMap2 (FF2,(n + p))) is with_the_same_dom by A10;

            

             A135: for i be Nat holds (( ProjMap2 (FF2,(n + p))) . i) is nonnegative by A38;

            x in ( dom (( ProjMap2 (FF2,(n + p))) . 0 )) by A1, A10, A23, A96;

            then (( Partial_Sums ( ProjMap2 (FF2,(n + p)))) # x) is non-decreasing by A134, A135, Th38;

            then ((( Partial_Sums ( ProjMap2 (FF2,(n + p)))) # x) . n9) <= ((( Partial_Sums ( ProjMap2 (FF2,(n + p)))) # x) . (n9 + p)) by A133, RINFSUP2: 7;

            then

             A136: ((( Partial_Sums ( ProjMap2 (FF2,(n + p)))) # x) . n9) <= ((( Partial_Sums ( ProjMap2 (FF2,(n + p)))) . (n + p)) . x) by MESFUNC5:def 13;

            (((P # x) ^\ n9) . p) = ((P # x) . (n + p)) by NAT_1:def 3;

            then (((P # x) ^\ n9) . p) = ((P . (n + p)) . x) by MESFUNC5:def 13;

            then

             A137: (((P # x) ^\ n9) . p) = ((( Partial_Sums ( ProjMap2 (FF2,(n + p)))) . (n + p)) . x) by A9;

            (((( ProjMap2 (PP2,n)) # x) ^\ n9) . p) = ((( ProjMap2 (PP2,n)) # x) . (n + p)) by NAT_1:def 3;

            then (((( ProjMap2 (PP2,n)) # x) ^\ n9) . p) = ((( ProjMap2 (PP2,n)) . (n + p)) . x) by MESFUNC5:def 13;

            then (((( ProjMap2 (PP2,n)) # x) ^\ n9) . p) = ((( Partial_Sums ( ProjMap2 (FF2,(n + p)))) . n) . x) by A98, A132;

            hence thesis by A137, A136, MESFUNC5:def 13;

          end;

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

          then

           A138: C[ 0 ] by A113, Def4;

          

           A139: for k be Nat holds C[k] from NAT_1:sch 2( A138, A116);

          ((P # x) ^\ n9) is convergent by A97, RINFSUP2: 21;

          then ( lim ((( ProjMap2 (PP2,n)) # x) ^\ n9)) <= ( lim ((P # x) ^\ n9)) by A115, A131, RINFSUP2: 38;

          then ( lim (( ProjMap2 (PP2,n)) # x)) <= ( lim (P # x)) by A99, A114;

          hence thesis by A139;

        end;

        (F # x) is summable by A1, A5, A23, A96;

        then

         A140: ( Partial_Sums (F # x)) is convergent;

        (( Partial_Sums F) # x) is convergent

        proof

          per cases by A140;

            suppose ( Partial_Sums (F # x)) is convergent_to_finite_number;

            then (( Partial_Sums F) # x) is convergent_to_finite_number by A2, A3, A23, A96, Th33;

            hence thesis;

          end;

            suppose ( Partial_Sums (F # x)) is convergent_to_+infty;

            then (( Partial_Sums F) # x) is convergent_to_+infty by A2, A3, A23, A96, Th33;

            hence thesis;

          end;

            suppose ( Partial_Sums (F # x)) is convergent_to_-infty;

            then (( Partial_Sums F) # x) is convergent_to_-infty by A2, A3, A23, A96, Th33;

            hence thesis;

          end;

        end;

        then

         A141: ( lim (( Partial_Sums F) # x)) <= ( lim (P # x)) by A111, Th9;

        

         A142: for k be Nat holds ((P # x) . k) <= ((( Partial_Sums F) # x) . k)

        proof

          let n be Nat;

          n in NAT by ORDINAL1:def 12;

          hence thesis by A31, A96;

        end;

        (( Partial_Sums F) # x) is convergent by A3, A4, A23, A96, Th38;

        then ( lim (P # x)) <= ( lim (( Partial_Sums F) # x)) by A97, A142, RINFSUP2: 38;

        hence thesis by A141, XXREAL_0: 1;

      end;

      

       A143: for x be Element of X st x in ( dom ( lim ( Partial_Sums F))) holds (P # x) is convergent & ( lim (P # x)) = (( lim ( Partial_Sums F)) . x)

      proof

        let x be Element of X;

        assume

         A144: x in ( dom ( lim ( Partial_Sums F)));

        then x in ( dom ( lim P)) by A1, A6, A22, A37;

        hence (P # x) is convergent by A91;

        ( lim (P # x)) = ( lim (( Partial_Sums F) # x)) by A1, A23, A37, A93, A144;

        hence thesis by A144, MESFUNC8:def 9;

      end;

      

       A145: for n be Nat holds (P . n) is nonnegative

      proof

        let n be Nat;

        for k be Nat holds (( ProjMap2 (FF2,n)) . k) is nonnegative by A38;

        then (( Partial_Sums ( ProjMap2 (FF2,n))) . n) is nonnegative by Th36;

        hence thesis by A9;

      end;

      

       A146: for x be object st x in ( dom ( lim ( Partial_Sums F))) holds (( lim ( Partial_Sums F)) . x) >= 0

      proof

        let x be object;

        assume

         A147: x in ( dom ( lim ( Partial_Sums F)));

        then

        reconsider x1 = x as Element of X;

        

         A148: for n be Nat holds ((( Partial_Sums F) # x1) . n) >= 0

        proof

          let n be Nat;

          (( Partial_Sums F) . n) is nonnegative by A4, Th36;

          then ((( Partial_Sums F) . n) . x1) >= 0 by SUPINF_2: 51;

          hence thesis by MESFUNC5:def 13;

        end;

        x in ( dom (F . 0 )) by A67, A147, Def4;

        then (( Partial_Sums F) # x1) is convergent by A3, A4, Th38;

        then ( lim (( Partial_Sums F) # x1)) >= 0 by A148, Th10;

        hence thesis by A147, MESFUNC8:def 9;

      end;

      then

       A149: ( lim ( Partial_Sums F)) is nonnegative by SUPINF_2: 52;

      consider I be ExtREAL_sequence such that

       A150: for n be Nat holds (I . n) = ( Integral (M,(F . n))) & ( Integral (M,(( Partial_Sums F) . n))) = (( Partial_Sums I) . n) by A1, A2, A3, A4, Th50;

      for n be object st n in ( dom I) holds 0 <= (I . n)

      proof

        let n be object;

        assume n in ( dom I);

        then

        reconsider n1 = n as Nat;

        

         A151: (F . n1) is nonnegative by A4;

        

         A152: (F . n1) is E -measurable by A4;

        E = ( dom (F . n1)) by A1, A3;

        then 0 <= ( Integral (M,(F . n1))) by A151, A152, MESFUNC5: 90;

        hence thesis by A150;

      end;

      then I is nonnegative by SUPINF_2: 52;

      then

       A153: ( Partial_Sums I) is non-decreasing by Th16;

      then

       A154: ( Partial_Sums I) is convergent by RINFSUP2: 37;

      deffunc J( Element of NAT ) = ( integral' (M,(P . $1)));

      consider J be sequence of ExtREAL such that

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

      reconsider J as ExtREAL_sequence;

      

       A156: for n be Nat holds (P . n) is_simple_func_in S

      proof

        let n be Nat;

        for m be Nat holds (( ProjMap2 (FF2,n)) . m) is_simple_func_in S by A10;

        then (( Partial_Sums ( ProjMap2 (FF2,n))) . n) is_simple_func_in S by Th35;

        hence thesis by A9;

      end;

      

       A157: for n be Nat holds (J . n) = ( integral' (M,(P . n)))

      proof

        let n be Nat;

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

        (J . n) = ( integral' (M,(P . n9))) by A155;

        hence thesis;

      end;

      for n,m be Nat st m <= n holds (J . m) <= (J . n)

      proof

        let n,m be Nat;

        

         A158: (P . n) is nonnegative by A145;

        

         A159: (P . m) is_simple_func_in S by A156;

        

         A160: for n,m,l be Nat holds ( dom ((P . n) - (P . m))) = ( dom (P . l))

        proof

          let n,m,l be Nat;

          (P . m) is_simple_func_in S by A156;

          then

           A161: (P . m) is without+infty by MESFUNC5: 14;

          (P . n) is_simple_func_in S by A156;

          then (P . n) is without-infty by MESFUNC5: 14;

          then ( dom ((P . n) - (P . m))) = (( dom (P . n)) /\ ( dom (P . m))) by A161, MESFUNC5: 17;

          then ( dom ((P . n) - (P . m))) = (( dom ( lim ( Partial_Sums F))) /\ ( dom (P . m))) by A69;

          then ( dom ((P . n) - (P . m))) = (( dom ( lim ( Partial_Sums F))) /\ ( dom ( lim ( Partial_Sums F)))) by A69;

          hence thesis by A69;

        end;

        then

         A162: ( dom ((P . n) - (P . m))) = ( dom (P . n));

        then

         A163: ((P . n) | ( dom ((P . n) - (P . m)))) = (P . n);

        assume

         A164: m <= n;

        

         A165: for x be object st x in ( dom ((P . n) - (P . m))) holds ((P . m) . x) <= ((P . n) . x)

        proof

          let x be object;

          assume x in ( dom ((P . n) - (P . m)));

          then x in ( dom ( lim ( Partial_Sums F))) by A69, A162;

          hence thesis by A68, A85, A164;

        end;

        

         A166: (P . m) is nonnegative by A145;

        ( dom ((P . n) - (P . m))) = ( dom (P . m)) by A160;

        then

         A167: ((P . m) | ( dom ((P . n) - (P . m)))) = (P . m);

        (P . n) is_simple_func_in S by A156;

        then ( integral' (M,((P . m) | ( dom ((P . n) - (P . m)))))) <= ( integral' (M,((P . n) | ( dom ((P . n) - (P . m)))))) by A158, A159, A166, A165, MESFUNC5: 70;

        then (J . m) <= ( integral' (M,(P . n))) by A157, A167, A163;

        hence thesis by A157;

      end;

      then J is non-decreasing by RINFSUP2: 7;

      then

       A168: J is convergent by RINFSUP2: 37;

      

       A169: for n be Nat holds (F . n) is without-infty by A4, MESFUNC5: 12;

      then

       A170: for n be Nat holds (( Partial_Sums F) . n) is E -measurable by A4, Th41;

      then ( lim ( Partial_Sums F)) is E -measurable by A1, A2, A3, A5, Th44;

      then ( integral+ (M,( lim ( Partial_Sums F)))) = ( lim J) by A68, A156, A85, A157, A69, A143, A145, A149, A168, MESFUNC5:def 15;

      then

       A171: ( Integral (M,( lim ( Partial_Sums F)))) = ( lim J) by A1, A2, A3, A5, A170, A37, A149, Th44, MESFUNC5: 88;

      

       A172: for n be Nat, x be Element of X st x in ( dom (F . n)) holds ((FF . n) # x) is non-decreasing

      proof

        let n be Nat, x be Element of X;

        assume

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

        let i,j be ExtReal;

        assume that

         A174: i in ( dom ((FF . n) # x)) and

         A175: j in ( dom ((FF . n) # x)) and

         A176: i <= j;

        reconsider i, j as Element of NAT by A174, A175;

        (((FF . n) . i) . x) <= (((FF . n) . j) . x) by A6, A173, A176;

        then (((FF . n) # x) . i) <= (((FF . n) . j) . x) by MESFUNC5:def 13;

        hence thesis by MESFUNC5:def 13;

      end;

      

       A177: for n,p be Nat st p >= n holds for x be Element of X st x in E holds ((( Partial_Sums ( ProjMap2 (FF2,p))) . n) . x) <= ((P . p) . x) & ((P . p) . x) = ((( Partial_Sums ( ProjMap2 (FF2,p))) . p) . x) & ((( Partial_Sums ( ProjMap2 (FF2,p))) . p) . x) <= ((( Partial_Sums F) . p) . x) & ((( Partial_Sums F) . p) . x) <= (( lim ( Partial_Sums F)) . x)

      proof

        let n,p be Nat;

        reconsider p1 = p, n1 = n as Element of NAT by ORDINAL1:def 12;

        assume

         A178: p >= n;

        let x be Element of X;

        

         A179: for i be Nat holds (( ProjMap2 (FF2,p)) . i) is nonnegative by A38;

        assume

         A180: x in E;

        then

         A181: x in ( dom (( ProjMap2 (FF2,p)) . 0 )) by A10;

        ( ProjMap2 (FF2,p)) is with_the_same_dom by A10;

        then (( Partial_Sums ( ProjMap2 (FF2,p))) # x) is non-decreasing by A181, A179, Th38;

        then ((( Partial_Sums ( ProjMap2 (FF2,p))) # x) . n1) <= ((( Partial_Sums ( ProjMap2 (FF2,p))) # x) . p1) by A178, RINFSUP2: 7;

        then ((( Partial_Sums ( ProjMap2 (FF2,p))) . n) . x) <= ((( Partial_Sums ( ProjMap2 (FF2,p))) # x) . p) by MESFUNC5:def 13;

        then ((( Partial_Sums ( ProjMap2 (FF2,p))) . n) . x) <= ((( Partial_Sums ( ProjMap2 (FF2,p))) . p) . x) by MESFUNC5:def 13;

        hence ((( Partial_Sums ( ProjMap2 (FF2,p))) . n) . x) <= ((P . p) . x) by A9;

        thus ((P . p) . x) = ((( Partial_Sums ( ProjMap2 (FF2,p))) . p) . x) by A9;

        

         A182: ( ProjMap2 (FF2,p)) is additive by A10;

        

         A183: ( ProjMap2 (FF2,p)) is with_the_same_dom by A10;

        

         A184: for n be Nat, x be Element of X st x in (( dom (( ProjMap2 (FF2,p)) . 0 )) /\ ( dom (F . 0 ))) holds ((( ProjMap2 (FF2,p)) . n) . x) <= ((F . n) . x)

        proof

          let n be Nat, x be Element of X;

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

          assume x in (( dom (( ProjMap2 (FF2,p)) . 0 )) /\ ( dom (F . 0 )));

          then x in ( dom (F . 0 )) by XBOOLE_0:def 4;

          then

           A185: x in ( dom (F . n)) by A3;

          then ((FF . n) # x) is non-decreasing by A172;

          then ( lim ((FF . n) # x)) = ( sup ((FF . n) # x)) by RINFSUP2: 37;

          then (((FF . n) # x) . p1) <= ( lim ((FF . n) # x)) by RINFSUP2: 23;

          then

           A186: (((FF . n) # x) . p) <= ((F . n) . x) by A6, A185;

          ((( ProjMap2 (FF2,p)) . n) . x) = ((FF2 . (n1,p1)) . x) by Def9;

          then ((( ProjMap2 (FF2,p)) . n) . x) = (((FF . n) . p) . x) by A8;

          hence thesis by A186, MESFUNC5:def 13;

        end;

        x in (( dom (( ProjMap2 (FF2,p)) . 0 )) /\ ( dom (F . 0 ))) by A1, A180, A181, XBOOLE_0:def 4;

        hence ((( Partial_Sums ( ProjMap2 (FF2,p))) . p) . x) <= ((( Partial_Sums F) . p) . x) by A2, A3, A182, A183, A184, Th42;

        (( Partial_Sums F) # x) is non-decreasing by A1, A3, A4, A180, Th38;

        then ( lim (( Partial_Sums F) # x)) = ( sup (( Partial_Sums F) # x)) by RINFSUP2: 37;

        then ((( Partial_Sums F) # x) . p1) <= ( lim (( Partial_Sums F) # x)) by RINFSUP2: 23;

        then ((( Partial_Sums F) . p) . x) <= ( lim (( Partial_Sums F) # x)) by MESFUNC5:def 13;

        hence thesis by A68, A180, MESFUNC8:def 9;

      end;

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

      proof

        let n be Nat;

        

         A187: (( Partial_Sums F) . n) is nonnegative by A4, Th36;

        

         A188: ( lim ( Partial_Sums F)) is E -measurable by A1, A2, A3, A5, A170, Th44;

        

         A189: (( Partial_Sums F) . n) is E -measurable by A4, A169, Th41;

        

         A190: E = ( dom (( Partial_Sums F) . n)) by A1, A2, A3, Th29;

        then for x be Element of X st x in ( dom (( Partial_Sums F) . n)) holds ((( Partial_Sums F) . n) . x) <= (( lim ( Partial_Sums F)) . x) by A177;

        then ( integral+ (M,(( Partial_Sums F) . n))) <= ( integral+ (M,( lim ( Partial_Sums F)))) by A37, A149, A190, A189, A188, A187, MESFUNC5: 85;

        then ( Integral (M,(( Partial_Sums F) . n))) <= ( integral+ (M,( lim ( Partial_Sums F)))) by A170, A190, A187, MESFUNC5: 88;

        then ( Integral (M,(( Partial_Sums F) . n))) <= ( Integral (M,( lim ( Partial_Sums F)))) by A37, A146, A188, MESFUNC5: 88, SUPINF_2: 52;

        hence thesis by A150;

      end;

      then

       A191: ( lim ( Partial_Sums I)) <= ( Integral (M,( lim ( Partial_Sums F)))) by A153, Th9, RINFSUP2: 37;

      take I;

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

      proof

        let n be Nat;

        ( dom (F . 0 )) = ( dom (F . n)) by A3;

        then ((F . n) | E) = (F . n) by A1;

        hence thesis by A150;

      end;

      

       A192: for n be Nat holds (J . n) = ( Integral (M,(P . n)))

      proof

        let n be Nat;

        

         A193: (P . n) is nonnegative by A145;

        

         A194: (J . n) = ( integral' (M,(P . n))) by A157;

        (P . n) is_simple_func_in S by A156;

        hence thesis by A193, A194, MESFUNC5: 89;

      end;

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

      proof

        let n be Nat;

        

         A195: (P . n) is E -measurable by A156, MESFUNC2: 34;

        

         A196: (( Partial_Sums F) . n) is nonnegative by A4, Th36;

        

         A197: n in NAT by ORDINAL1:def 12;

        

         A198: for x be Element of X st x in ( dom (P . n)) holds ((P . n) . x) <= ((( Partial_Sums F) . n) . x)

        proof

          let x be Element of X;

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

          then x in ( dom ( lim ( Partial_Sums F))) by A69;

          then ((P # x) . n) <= ((( Partial_Sums F) # x) . n) by A1, A23, A37, A31, A197;

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

          hence thesis by MESFUNC5:def 13;

        end;

        

         A199: (P . n) is nonnegative by A145;

        

         A200: ( dom (P . n)) = E by A37, A69;

        

         A201: E = ( dom (( Partial_Sums F) . n)) by A1, A2, A3, Th29;

        (( Partial_Sums F) . n) is E -measurable by A4, A169, Th41;

        then ( integral+ (M,(P . n))) <= ( integral+ (M,(( Partial_Sums F) . n))) by A201, A200, A195, A199, A196, A198, MESFUNC5: 85;

        then ( Integral (M,(P . n))) <= ( integral+ (M,(( Partial_Sums F) . n))) by A145, A200, A195, MESFUNC5: 88;

        then ( Integral (M,(P . n))) <= ( Integral (M,(( Partial_Sums F) . n))) by A170, A201, A196, MESFUNC5: 88;

        then (J . n) <= ( Integral (M,(( Partial_Sums F) . n))) by A192;

        hence thesis by A150;

      end;

      then ( lim J) <= ( lim ( Partial_Sums I)) by A168, A154, RINFSUP2: 38;

      then ( Sum I) = ( Integral (M,( lim ( Partial_Sums F)))) by A171, A191, XXREAL_0: 1;

      hence thesis by A37, A154;

    end;

    theorem :: MESFUNC9:51

    

     Th51: E c= ( dom (F . 0 )) & F is additive & F is with_the_same_dom & (for n be Nat holds (F . n) is nonnegative & (F . n) is E -measurable) & (for x be Element of X st x in E holds (F # x) is summable) implies ex I be ExtREAL_sequence st (for n be Nat holds (I . n) = ( Integral (M,((F . n) | E)))) & I is summable & ( Integral (M,(( lim ( Partial_Sums F)) | E))) = ( Sum I)

    proof

      assume that

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

       A2: F is additive and

       A3: F is with_the_same_dom and

       A4: for n be Nat holds (F . n) is nonnegative & (F . n) is E -measurable and

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

      deffunc F( Nat) = ((F . $1) | E);

      consider G be Functional_Sequence of X, ExtREAL such that

       A6: for n be Nat holds (G . n) = F(n) from SEQFUNC:sch 1;

      reconsider G as additive with_the_same_dom Functional_Sequence of X, ExtREAL by A2, A3, A6, Th18, Th31;

      

       A7: for n be Nat holds (G . n) is nonnegative & (G . n) is E -measurable

      proof

        let n be Nat;

        ((F . n) | E) is nonnegative by A4, MESFUNC5: 15;

        hence (G . n) is nonnegative by A6;

        thus thesis by A1, A3, A4, A6, Th20;

      end;

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

      then

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

      

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

      proof

        let x be Element of X;

        assume

         A10: x in E;

        for n9 be object st n9 in NAT holds ((F # x) . n9) = ((G # x) . n9)

        proof

          let n9 be object;

          assume n9 in NAT ;

          then

          reconsider n = n9 as Nat;

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

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

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

          then

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

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

          hence thesis by A11, MESFUNC5:def 13;

        end;

        hence thesis;

      end;

      

       A12: (( lim ( Partial_Sums G)) | E) = (( lim ( Partial_Sums F)) | E)

      proof

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

        set PF = ( Partial_Sums F);

        set PG = ( Partial_Sums G);

        

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

        ( dom (PF . 0 )) = E1 by A2, A3, Th29;

        then

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

        

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

        proof

          let x be Element of X;

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

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

          assume

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

          then

           A17: x in E by A8, A13, Th29;

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

          proof

            let n be Element of NAT ;

            

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

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

            hence thesis by A9, A17, A18;

          end;

          then

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

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

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

        end;

        

         A20: ( dom (PG . 0 )) = ( dom (G . 0 )) by Th29;

        then

         A21: ( dom (( lim PG) | E)) = ( dom ( lim PG)) by A8, A13;

        

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

        then

         A23: ( dom (( lim PG) | E)) = ( dom (( lim PF) | E)) by A8, A20, A13;

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

        proof

          let x be Element of X;

          assume

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

          then

           A25: ((( lim PF) | E) . x) = (( lim PF) . x) by A23, FUNCT_1: 47;

          (( lim PG) . x) = (( lim PF) . x) by A21, A15, A24;

          hence thesis by A24, A25, FUNCT_1: 47;

        end;

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

      end;

      for x be Element of X st x in E holds (G # x) is summable by A1, A5, A6, Th21;

      then

      consider I be ExtREAL_sequence such that

       A26: for n be Nat holds (I . n) = ( Integral (M,((G . n) | E))) and

       A27: I is summable and

       A28: ( Integral (M,(( lim ( Partial_Sums G)) | E))) = ( Sum I) by A8, A7, Lm4;

      take I;

      now

        let n be Nat;

        (((F . n) | E) | E) = ((F . n) | E);

        then ((G . n) | E) = ((F . n) | E) by A6;

        hence (I . n) = ( Integral (M,((F . n) | E))) by A26;

      end;

      hence thesis by A27, A28, A12;

    end;

    ::$Notion-Name

    theorem :: MESFUNC9:52

    E = ( dom (F . 0 )) & (F . 0 ) is nonnegative & F is with_the_same_dom & (for n be Nat holds (F . n) is E -measurable) & (for n,m be Nat st n <= m holds for x be Element of X st x in E holds ((F . n) . x) <= ((F . m) . x)) & (for x be Element of X st x in E holds (F # x) is convergent) implies ex I be ExtREAL_sequence st (for n be Nat holds (I . n) = ( Integral (M,(F . n)))) & I is convergent & ( Integral (M,( lim F))) = ( lim I)

    proof

      assume that

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

       A2: (F . 0 ) is nonnegative and

       A3: F is with_the_same_dom and

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

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

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

      

       A7: ( lim F) is E -measurable by A1, A3, A4, A6, MESFUNC8: 25;

      

       A8: for n be Nat holds (F . n) is nonnegative

      proof

        let n be Nat;

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

        proof

          let x be object;

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

          then x in E by A1, A3;

          then ((F . 0 ) . x) <= ((F . n) . x) by A5;

          hence thesis by A2, SUPINF_2: 51;

        end;

        hence thesis by SUPINF_2: 52;

      end;

      per cases ;

        suppose ex n be Nat st (M . (E /\ ( eq_dom ((F . n), +infty )))) <> 0 ;

        then

        consider N be Nat such that

         A9: (M . (E /\ ( eq_dom ((F . N), +infty )))) <> 0 ;

        

         A10: E = ( dom (F . N)) by A1, A3;

        then

        reconsider EE = (E /\ ( eq_dom ((F . N), +infty ))) as Element of S by A4, MESFUNC1: 33;

        

         A11: EE c= E by XBOOLE_1: 17;

        then

         A12: (F . N) is EE -measurable by A4, MESFUNC1: 30;

        EE c= ( dom (F . N)) by A1, A3, A11;

        then

         A13: EE = ( dom ((F . N) | EE)) by RELAT_1: 62;

        then EE = (( dom (F . N)) /\ EE) by RELAT_1: 61;

        then

         A14: ((F . N) | EE) is EE -measurable by A12, MESFUNC5: 42;

        now

          let x be object;

          assume

           A15: x in EE;

          then x in ( eq_dom ((F . N), +infty )) by XBOOLE_0:def 4;

          then ((F . N) . x) = +infty by MESFUNC1:def 15;

          then (((F . N) | EE) . x) = +infty by A13, A15, FUNCT_1: 47;

          hence x in ( eq_dom (((F . N) | EE), +infty )) by A13, A15, MESFUNC1:def 15;

        end;

        then

         A16: EE c= ( eq_dom (((F . N) | EE), +infty ));

        for x be object st x in ( eq_dom (((F . N) | EE), +infty )) holds x in EE by A13, MESFUNC1:def 15;

        then ( eq_dom (((F . N) | EE), +infty )) c= EE;

        then EE = ( eq_dom (((F . N) | EE), +infty )) by A16, XBOOLE_0:def 10;

        then

         A17: (M . (EE /\ ( eq_dom (((F . N) | EE), +infty )))) <> 0 by A9;

        (F . N) is E -measurable by A4;

        then

         A18: ( Integral (M,((F . N) | EE))) <= ( Integral (M,((F . N) | E))) by A8, A10, A11, MESFUNC5: 93;

        reconsider N1 = N as Element of NAT by ORDINAL1:def 12;

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

        consider I be sequence of ExtREAL such that

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

        reconsider I as ExtREAL_sequence;

        

         A20: 0 < (M . (E /\ ( eq_dom ((F . N), +infty )))) by A9, SUPINF_2: 51;

        

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

        proof

          let n be Nat;

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

          (I . n) = ( Integral (M,(F . n1))) by A19;

          hence thesis;

        end;

        take I;

        

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

        for x be object st x in ( dom ( lim F)) holds (( lim F) . x) >= 0

        proof

          let x be object;

          assume

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

          then

          reconsider x1 = x as Element of X;

          for n be Nat holds ((F # x1) . n) >= 0

          proof

            let n be Nat;

            

             A24: ((F . 0 ) . x1) >= 0 by A2, SUPINF_2: 51;

            ((F . n) . x1) >= ((F . 0 ) . x1) by A1, A5, A22, A23;

            hence thesis by A24, MESFUNC5:def 13;

          end;

          then ( lim (F # x1)) >= 0 by A1, A6, A22, A23, Th10;

          hence thesis by A23, MESFUNC8:def 9;

        end;

        then

         A25: ( lim F) is nonnegative by SUPINF_2: 52;

        

         A26: E = ( dom ( lim F)) by A1, MESFUNC8:def 9;

        

         A27: EE c= (E /\ ( eq_dom (( lim F), +infty )))

        proof

          let x be object;

          assume

           A28: x in EE;

          then

          reconsider x1 = x as Element of X;

          x in ( eq_dom ((F . N), +infty )) by A28, XBOOLE_0:def 4;

          then ((F . N) . x1) = +infty by MESFUNC1:def 15;

          then

           A29: ((F # x1) . N) = +infty by MESFUNC5:def 13;

          

           A30: x in E by A28, XBOOLE_0:def 4;

          for n,m be Nat st m <= n holds ((F # x1) . m) <= ((F # x1) . n)

          proof

            let n,m be Nat;

            assume m <= n;

            then ((F . m) . x1) <= ((F . n) . x1) by A5, A30;

            then ((F # x1) . m) <= ((F . n) . x1) by MESFUNC5:def 13;

            hence thesis by MESFUNC5:def 13;

          end;

          then

           A31: (F # x1) is non-decreasing by RINFSUP2: 7;

          then

           A32: ((F # x1) ^\ N1) is non-decreasing by RINFSUP2: 26;

          (((F # x1) ^\ N1) . 0 ) = ((F # x1) . ( 0 + N)) by NAT_1:def 3;

          then for n be Element of NAT holds +infty <= (((F # x1) ^\ N1) . n) by A29, A32, RINFSUP2: 7;

          then ((F # x1) ^\ N1) is convergent_to_+infty by RINFSUP2: 32;

          then

           A33: ( lim ((F # x1) ^\ N1)) = +infty by Th7;

          

           A34: ( sup (F # x1)) = ( sup ((F # x1) ^\ N1)) by A31, RINFSUP2: 26;

          ( lim (F # x1)) = ( sup (F # x1)) by A31, RINFSUP2: 37;

          then ( lim (F # x1)) = +infty by A32, A34, A33, RINFSUP2: 37;

          then (( lim F) . x1) = +infty by A1, A22, A30, MESFUNC8:def 9;

          then x in ( eq_dom (( lim F), +infty )) by A26, A30, MESFUNC1:def 15;

          hence thesis by A30, XBOOLE_0:def 4;

        end;

        

         A35: for n,m be Nat st m <= n holds (I . m) <= (I . n)

        proof

          let n,m be Nat;

          

           A36: (F . m) is E -measurable by A4;

          assume m <= n;

          then

           A37: for x be Element of X st x in E holds ((F . m) . x) <= ((F . n) . x) by A5;

          

           A38: E = ( dom (F . m)) by A1, A3;

          

           A39: E = ( dom (F . n)) by A1, A3;

          

           A40: n in NAT by ORDINAL1:def 12;

          

           A41: m in NAT by ORDINAL1:def 12;

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

          then ( Integral (M,((F . m) | E))) <= ( Integral (M,((F . n) | E))) by A8, A38, A39, A36, A37, Th15;

          then ( Integral (M,(F . m))) <= ( Integral (M,((F . n) | E))) by A38;

          then ( Integral (M,(F . m))) <= ( Integral (M,(F . n))) by A39;

          then (I . m) <= ( Integral (M,(F . n))) by A19, A41;

          hence thesis by A19, A40;

        end;

        then

         A42: I is non-decreasing by RINFSUP2: 7;

        then

         A43: (I ^\ N1) is non-decreasing by RINFSUP2: 26;

        (F . N) is nonnegative by A8;

        then ( Integral (M,((F . N) | EE))) = +infty by A13, A14, A17, Th13, MESFUNC5: 15;

        then +infty <= ( Integral (M,(F . N))) by A10, A18;

        then

         A44: ( Integral (M,(F . N))) = +infty by XXREAL_0: 4;

        for k be Element of NAT holds +infty <= ((I ^\ N1) . k)

        proof

          let k be Element of NAT ;

          (I . N1) <= (I . (N1 + k)) by A35, NAT_1: 12;

          then (I . N1) <= ((I ^\ N1) . k) by NAT_1:def 3;

          hence thesis by A44, A21;

        end;

        then (I ^\ N1) is convergent_to_+infty by RINFSUP2: 32;

        then

         A45: ( lim (I ^\ N1)) = +infty by Th7;

        (E /\ ( eq_dom (( lim F), +infty ))) is Element of S by A7, A26, MESFUNC1: 33;

        then

         A46: (M . (E /\ ( eq_dom (( lim F), +infty )))) <> 0 by A27, A20, MEASURE1: 31;

        

         A47: ( sup I) = ( sup (I ^\ N1)) by A42, RINFSUP2: 26;

        ( lim I) = ( sup I) by A42, RINFSUP2: 37;

        then ( lim I) = +infty by A43, A47, A45, RINFSUP2: 37;

        hence thesis by A7, A21, A42, A26, A25, A46, Th13, RINFSUP2: 37;

      end;

        suppose

         A48: for n be Nat holds (M . (E /\ ( eq_dom ((F . n), +infty )))) = 0 ;

        defpred L[ Element of NAT , set] means $2 = (E /\ ( eq_dom ((F . $1), +infty )));

        

         A49: for n be Element of NAT holds ex A be Element of S st L[n, A]

        proof

          let n be Element of NAT ;

          E c= ( dom (F . n)) by A1, A3;

          then

          reconsider A = (E /\ ( eq_dom ((F . n), +infty ))) as Element of S by A4, MESFUNC1: 33;

          take A;

          thus thesis;

        end;

        consider L be sequence of S such that

         A50: for n be Element of NAT holds L[n, (L . n)] from FUNCT_2:sch 3( A49);

        

         A51: ( rng L) c= S by RELAT_1:def 19;

        ( rng L) is N_Sub_set_fam of X by MEASURE1: 23;

        then

        reconsider E0 = ( rng L) as N_Measure_fam of S by A51, MEASURE2:def 1;

        set E1 = (E \ ( union E0));

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

        consider H be Functional_Sequence of X, ExtREAL such that

         A52: for n be Nat holds (H . n) = H(n) from SEQFUNC:sch 1;

        deffunc I2( Element of NAT ) = ( Integral (M,((F . $1) | E1)));

        consider I be sequence of ExtREAL such that

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

        reconsider I as ExtREAL_sequence;

        

         A54: E1 c= E by XBOOLE_1: 36;

        then

         A55: for n be Nat holds (F . n) is E1 -measurable by A4, MESFUNC1: 30;

        

         A56: for n be Nat holds ( dom (H . n)) = E1 & (H . n) is without-infty & (H . n) is without+infty

        proof

          let n be Nat;

          

           A57: ( dom (H . n)) = ( dom ((F . n) | E1)) by A52;

          E1 c= ( dom (F . n)) by A1, A3, A54;

          hence ( dom (H . n)) = E1 by A57, RELAT_1: 62;

          ((F . n) | E1) is nonnegative by A8, MESFUNC5: 15;

          then (H . n) is nonnegative by A52;

          hence (H . n) is without-infty by MESFUNC5: 12;

          for x be set st x in ( dom (H . n)) holds ((H . n) . x) < +infty

          proof

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

            let x be set;

            

             A58: (L . n) = (E /\ ( eq_dom ((F . n1), +infty ))) by A50;

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

            then

             A59: (L . n) in ( rng L) by A58, FUNCT_1: 3;

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

            then

             A60: x in ( dom ((F . n) | E1)) by A52;

            then

             A61: x in E1 by RELAT_1: 57;

            

             A62: x in ( dom (F . n)) by A60, RELAT_1: 57;

            assume

             A63: ((H . n) . x) >= +infty ;

            ((H . n) . x) = (((F . n) | E1) . x) by A52;

            then ((H . n) . x) = ((F . n) . x) by A61, FUNCT_1: 49;

            then ((F . n) . x) = +infty by A63, XXREAL_0: 4;

            then x in ( eq_dom ((F . n), +infty )) by A62, MESFUNC1:def 15;

            then x in (L . n) by A54, A61, A58, XBOOLE_0:def 4;

            then x in ( union E0) by A59, TARSKI:def 4;

            hence contradiction by A61, XBOOLE_0:def 5;

          end;

          hence thesis by MESFUNC5: 11;

        end;

        for n,m be Nat holds ( dom (H . n)) = ( dom (H . m))

        proof

          let n,m be Nat;

          ( dom (H . n)) = E1 by A56;

          hence thesis by A56;

        end;

        then

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

        defpred G[ Nat, set, set] means $3 = ((H . ($1 + 1)) - (H . $1));

        

         A64: for n be Nat holds for x be set holds ex y be set st G[n, x, y];

        consider G be Function such that

         A65: ( dom G) = NAT & (G . 0 ) = (H . 0 ) & for n be Nat holds G[n, (G . n), (G . (n + 1))] from RECDEF_1:sch 1( A64);

        

         A66: for n be Nat holds (G . (n + 1)) = ((H . (n + 1)) - (H . n)) by A65;

        now

          defpred IND[ Nat] means (G . $1) is PartFunc of X, ExtREAL ;

          let f be object;

          assume f in ( rng G);

          then

          consider m be object such that

           A67: m in ( dom G) and

           A68: f = (G . m) by FUNCT_1:def 3;

          reconsider m as Nat by A65, A67;

          

           A69: for n be Nat st IND[n] holds IND[(n + 1)]

          proof

            let n be Nat;

            assume IND[n];

            (G . (n + 1)) = ((H . (n + 1)) - (H . n)) by A66;

            hence thesis;

          end;

          

           A70: IND[ 0 ] by A65;

          for n be Nat holds IND[n] from NAT_1:sch 2( A70, A69);

          then (G . m) is PartFunc of X, ExtREAL ;

          hence f in ( PFuncs (X, ExtREAL )) by A68, PARTFUN1: 45;

        end;

        then ( rng G) c= ( PFuncs (X, ExtREAL ));

        then

        reconsider G as Functional_Sequence of X, ExtREAL by A65, FUNCT_2:def 1, RELSET_1: 4;

        

         A71: for n be Nat holds ( dom (G . n)) = E1

        proof

          let n be Nat;

          now

            assume n <> 0 ;

            then

            consider k be Nat such that

             A72: n = (k + 1) by NAT_1: 6;

            

             A73: (H . (k + 1)) is without-infty by A56;

            

             A74: (H . k) is without+infty by A56;

            (G . (k + 1)) = ((H . (k + 1)) - (H . k)) by A66;

            then ( dom (G . (k + 1))) = (( dom (H . (k + 1))) /\ ( dom (H . k))) by A73, A74, MESFUNC5: 17;

            then ( dom (G . (k + 1))) = (E1 /\ ( dom (H . k))) by A56;

            then ( dom (G . (k + 1))) = (E1 /\ E1) by A56;

            hence thesis by A72;

          end;

          hence thesis by A56, A65;

        end;

        

         A75: for n,m be Nat holds ( dom (G . n)) = ( dom (G . m))

        proof

          let n,m be Nat;

          ( dom (G . n)) = E1 by A71;

          hence thesis by A71;

        end;

        

         A76: for n be Nat holds (G . n) is nonnegative

        proof

          let n be Nat;

          

           A77: n <> 0 implies (G . n) is nonnegative

          proof

            assume n <> 0 ;

            then

            consider k be Nat such that

             A78: n = (k + 1) by NAT_1: 6;

            

             A79: (G . (k + 1)) = ((H . (k + 1)) - (H . k)) by A66;

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

            proof

              let x be object;

              assume

               A80: x in ( dom (G . (k + 1)));

              

               A81: ( dom (G . (k + 1))) = E1 by A71;

              ((H . k) . x) = (((F . k) | E1) . x) by A52;

              then

               A82: ((H . k) . x) = ((F . k) . x) by A80, A81, FUNCT_1: 49;

              ((H . (k + 1)) . x) = (((F . (k + 1)) | E1) . x) by A52;

              then

               A83: ((H . (k + 1)) . x) = ((F . (k + 1)) . x) by A80, A81, FUNCT_1: 49;

              ((F . k) . x) <= ((F . (k + 1)) . x) by A5, A54, A80, A81, NAT_1: 11;

              then (((H . (k + 1)) . x) - ((H . k) . x)) >= 0 by A83, A82, XXREAL_3: 40;

              hence thesis by A79, A80, MESFUNC1:def 4;

            end;

            hence thesis by A78, SUPINF_2: 52;

          end;

          n = 0 implies (G . n) is nonnegative

          proof

            assume

             A84: n = 0 ;

            ((F . n) | E1) is nonnegative by A8, MESFUNC5: 15;

            hence thesis by A52, A65, A84;

          end;

          hence thesis by A77;

        end;

        

         A85: for n1 be object st n1 in NAT holds (H . n1) = (( Partial_Sums G) . n1)

        proof

          defpred PH[ Nat] means (H . $1) = (( Partial_Sums G) . $1);

          let n1 be object;

          assume n1 in NAT ;

          then

          reconsider n = n1 as Nat;

          

           A86: for k be Nat st PH[k] holds PH[(k + 1)]

          proof

            let k be Nat;

            

             A87: (H . k) is without+infty by A56;

            

             A88: (H . k) is without-infty by A56;

            

             A89: ( dom (G . (k + 1))) = E1 by A71;

            (G . (k + 1)) is without-infty by A76, MESFUNC5: 12;

            then ( dom ((G . (k + 1)) + (H . k))) = (( dom (G . (k + 1))) /\ ( dom (H . k))) by A88, MESFUNC5: 16;

            then ( dom ((G . (k + 1)) + (H . k))) = (E1 /\ E1) by A56, A89;

            then

             A90: ( dom (H . (k + 1))) = ( dom ((G . (k + 1)) + (H . k))) by A56;

            

             A91: (G . (k + 1)) = ((H . (k + 1)) - (H . k)) by A66;

            for x be Element of X st x in ( dom (H . (k + 1))) holds ((H . (k + 1)) . x) = (((G . (k + 1)) + (H . k)) . x)

            proof

              let x be Element of X;

              

               A92: ((H . k) . x) <> +infty by A87;

              ((H . k) . x) <> -infty by A88;

              then ((((H . (k + 1)) . x) - ((H . k) . x)) + ((H . k) . x)) = (((H . (k + 1)) . x) - (((H . k) . x) - ((H . k) . x))) by A92, XXREAL_3: 32;

              then ((((H . (k + 1)) . x) - ((H . k) . x)) + ((H . k) . x)) = (((H . (k + 1)) . x) - 0. ) by XXREAL_3: 7;

              then

               A93: ((((H . (k + 1)) . x) - ((H . k) . x)) + ((H . k) . x)) = ((H . (k + 1)) . x) by XXREAL_3: 4;

              assume

               A94: x in ( dom (H . (k + 1)));

              then x in E1 by A56;

              then ((H . (k + 1)) . x) = (((G . (k + 1)) . x) + ((H . k) . x)) by A91, A89, A93, MESFUNC1:def 4;

              hence thesis by A90, A94, MESFUNC1:def 3;

            end;

            then

             A95: (H . (k + 1)) = ((G . (k + 1)) + (H . k)) by A90, PARTFUN1: 5;

            assume PH[k];

            hence thesis by A95, Def4;

          end;

          

           A96: PH[ 0 ] by A65, Def4;

          for k be Nat holds PH[k] from NAT_1:sch 2( A96, A86);

          then (H . n) = (( Partial_Sums G) . n);

          hence thesis;

        end;

        then

         A97: for n be Nat holds (H . n) = (( Partial_Sums G) . n) & ( lim H) = ( lim ( Partial_Sums G)) by FUNCT_2: 12;

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

        reconsider G as additive with_the_same_dom Functional_Sequence of X, ExtREAL by A76, Th30;

        

         A98: for k be Nat holds (H . k) is real-valued

        proof

          let k be Nat;

          for x be Element of X st x in ( dom (H . k)) holds |.((H . k) . x).| < +infty

          proof

            let x be Element of X;

            assume x in ( dom (H . k));

            (H . k) is without+infty by A56;

            then

             A99: ((H . k) . x) < +infty ;

            (H . k) is without-infty by A56;

            then -infty < ((H . k) . x);

            hence thesis by A99, EXTREAL1: 40, XXREAL_0: 4;

          end;

          hence thesis by MESFUNC2:def 1;

        end;

        

         A100: for n be Nat holds (G . n) is E1 -measurable

        proof

          let n be Nat;

          n <> 0 implies (G . n) is E1 -measurable

          proof

            assume n <> 0 ;

            then

            consider k be Nat such that

             A101: n = (k + 1) by NAT_1: 6;

            

             A102: E1 = ( dom (H . k)) by A56;

            

             A103: (G . (k + 1)) = ((H . (k + 1)) - (H . k)) by A66;

            

             A104: (H . k) is real-valued by A98;

            

             A105: (H . k) is E1 -measurable by A1, A3, A55, A52, Th20, XBOOLE_1: 36;

            

             A106: (H . (k + 1)) is real-valued by A98;

            (H . (k + 1)) is E1 -measurable by A1, A3, A55, A52, Th20, XBOOLE_1: 36;

            hence thesis by A101, A105, A102, A106, A104, A103, MESFUNC2: 11;

          end;

          hence thesis by A1, A3, A54, A55, A52, A65, Th20;

        end;

        

         A107: E1 = ( dom (G . 0 )) by A56, A65;

        for x be Element of X st x in E1 holds (G # x) is summable

        proof

          let x be Element of X;

          assume

           A108: x in E1;

          E1 c= E by XBOOLE_1: 36;

          then (F # x) is convergent by A6, A108;

          then (H # x) is convergent by A52, A108, Th12;

          then (( Partial_Sums G) # x) is convergent by A85, FUNCT_2: 12;

          then ( Partial_Sums (G # x)) is convergent by A107, A108, Th33;

          hence thesis;

        end;

        then

        consider J be ExtREAL_sequence such that

         A109: for n be Nat holds (J . n) = ( Integral (M,((G . n) | E1))) and J is summable and

         A110: ( Integral (M,(( lim ( Partial_Sums G)) | E1))) = ( Sum J) by A76, A107, A100, Th51;

        for n be object st n in NAT holds (I . n) = (( Partial_Sums J) . n)

        proof

          let n be object;

          assume n in NAT ;

          then

          reconsider n1 = n as Element of NAT ;

          

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

          proof

            let n be Nat;

            ( dom (G . n)) = E1 by A71;

            then ((G . n) | E1) = (G . n);

            hence thesis by A109;

          end;

          E1 = ( dom (G . 0 )) by A71;

          then (( Partial_Sums J) . n1) = ( Integral (M,(( Partial_Sums G) . n1))) by A76, A100, A111, Th46;

          then (( Partial_Sums J) . n1) = ( Integral (M,(H . n1))) by A85;

          then (( Partial_Sums J) . n1) = ( Integral (M,((F . n1) | E1))) by A52;

          hence thesis by A53;

        end;

        then

         A112: I = ( Partial_Sums J);

        ( dom ( lim ( Partial_Sums G))) = ( dom (H . 0 )) by A97, MESFUNC8:def 9;

        then ( dom ( lim ( Partial_Sums G))) = E1 by A56;

        then

         A113: ( lim I) = ( Integral (M,( lim H))) by A97, A110, A112;

        take I;

        

         A114: for x be Element of X st x in E1 holds (F # x) is convergent

        proof

          let x be Element of X;

          

           A115: E1 c= E by XBOOLE_1: 36;

          assume x in E1;

          hence thesis by A6, A115;

        end;

        

         A116: for n be Element of NAT st 0 <= n holds ((M * L) . n) = 0

        proof

          let n be Element of NAT ;

          assume 0 <= n;

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

          then ((M * L) . n) = (M . (L . n)) by FUNCT_1: 13;

          then ((M * L) . n) = (M . (E /\ ( eq_dom ((F . n), +infty )))) by A50;

          hence thesis by A48;

        end;

        (M * L) is nonnegative by MEASURE2: 1;

        then ( SUM (M * L)) = (( Ser (M * L)) . 0 ) by A116, SUPINF_2: 48;

        then ( SUM (M * L)) = ((M * L) . 0 ) by SUPINF_2:def 11;

        then ( SUM (M * L)) = 0 by A116;

        then (M . ( union E0)) <= 0 by MEASURE2: 11;

        then

         A117: (M . ( union E0)) = 0 by SUPINF_2: 51;

        

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

        proof

          let n be Nat;

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

          

           A119: (I . n) = ( Integral (M,((F . n1) | E1))) by A53;

          ( dom (F . n)) = E by A1, A3;

          hence thesis by A4, A117, A119, MESFUNC5: 95;

        end;

        for n,m be Nat st m <= n holds (I . m) <= (I . n)

        proof

          let n,m be Nat;

          

           A120: (F . m) is nonnegative by A8;

          

           A121: ( dom (F . m)) = E by A1, A3;

          assume m <= n;

          then

           A122: for x be Element of X st x in ( dom (F . m)) holds ((F . m) . x) <= ((F . n) . x) by A5, A121;

          

           A123: ( dom (F . n)) = E by A1, A3;

          

           A124: (F . n) is E -measurable by A4;

          

           A125: (F . n) is nonnegative by A8;

          (F . m) is E -measurable by A4;

          then ( integral+ (M,(F . m))) <= ( integral+ (M,(F . n))) by A121, A123, A122, A120, A125, A124, MESFUNC5: 85;

          then ( Integral (M,(F . m))) <= ( integral+ (M,(F . n))) by A4, A121, A120, MESFUNC5: 88;

          then ( Integral (M,(F . m))) <= ( Integral (M,(F . n))) by A4, A123, A125, MESFUNC5: 88;

          then (I . m) <= ( Integral (M,(F . n))) by A118;

          hence thesis by A118;

        end;

        then

         A126: I is non-decreasing by RINFSUP2: 7;

        E = ( dom ( lim F)) by A1, MESFUNC8:def 9;

        then

         A127: ( Integral (M,( lim F))) = ( Integral (M,(( lim F) | E1))) by A7, A117, MESFUNC5: 95;

        E1 c= ( dom (F . 0 )) by A1, XBOOLE_1: 36;

        hence thesis by A127, A52, A118, A126, A114, A113, Th19, RINFSUP2: 37;

      end;

    end;