mesfun9c.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 for Functional_Sequence of X, REAL ,

f for PartFunc of X, REAL ,

seq for Real_Sequence,

n,m for Nat,

x for Element of X,

z,D for set;

    definition

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

      let D be set;

      :: MESFUN9C:def1

      func F || D -> Functional_Sequence of X, Y means

      : Def1: for n be Nat holds (it . n) = ((F . n) | D);

      existence

      proof

        deffunc F( Nat) = ((F . $1) | D);

        ex G be Functional_Sequence of X, Y st for n be Nat holds (G . n) = F(n) from SEQFUNC:sch 1;

        hence thesis;

      end;

      uniqueness

      proof

        let A,B be Functional_Sequence of X, Y such that

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

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

        let x be Element of NAT ;

        

        thus (A . x) = ((F . x) | D) by A1

        .= (B . x) by A2;

      end;

    end

    theorem :: MESFUN9C:1

    

     Th1: x in D & (F # x) is convergent implies ((F || D) # x) is convergent

    proof

      set G = (F || D);

      assume

       A1: x in D;

      

       A2: (( R_EAL G) # x) = (G # x) by MESFUN7C: 1;

      assume (F # x) is convergent;

      then ( R_EAL (F # x)) is convergent_to_finite_number by RINFSUP2: 14;

      then

       A3: (( R_EAL F) # x) is convergent_to_finite_number by MESFUN7C: 1;

      for n be Nat holds (( R_EAL G) . n) = ((( R_EAL F) . n) | D) by Def1;

      then (( R_EAL G) # x) is convergent_to_finite_number by A1, A3, MESFUNC9: 12;

      hence thesis by A2, RINFSUP2: 15;

    end;

    theorem :: MESFUN9C:2

    

     Th2: for X,Y,D be set, F be Functional_Sequence of X, Y st F is with_the_same_dom holds (F || D) is with_the_same_dom

    proof

      let X,Y,D be set, F be Functional_Sequence of X, Y;

      assume

       A1: F is with_the_same_dom;

      let n,m be Nat;

      set G = (F || D);

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

      then

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

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

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

      hence ( dom (G . n)) = ( dom (G . m)) by A1, A2;

    end;

    theorem :: MESFUN9C:3

    

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

    proof

      set G = (F || D);

      assume that

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

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

      

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

      proof

        let x be Element of X;

        assume x in D;

        then

         A4: (F # x) is convergent by A2;

        (( R_EAL F) # x) = (F # x) by MESFUN7C: 1;

        hence (( R_EAL F) # x) is convergent by A4, RINFSUP2: 14;

      end;

      for n be Nat holds (( R_EAL G) . n) = ((( R_EAL F) . n) | D) by Def1;

      hence (( lim F) | D) = ( lim G) by A1, A3, MESFUNC9: 19;

    end;

    theorem :: MESFUN9C:4

    

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

    proof

      set G = (F || E);

      assume

       A1: F is with_the_same_dom & E c= ( dom (F . 0 ));

      assume

       A2: for m be Nat holds (F . m) is E -measurable;

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

      proof

        let m be Nat;

        (F . m) is E -measurable by A2;

        then ( R_EAL (F . m)) is E -measurable;

        hence (( R_EAL F) . m) is E -measurable;

        thus (( R_EAL G) . m) = ((( R_EAL F) . m) | E) by Def1;

      end;

      then ( R_EAL (G . n)) is E -measurable by A1, MESFUNC9: 20;

      hence (G . n) is E -measurable;

    end;

    reserve i for Element of NAT ;

    theorem :: MESFUN9C:5

    

     Th5: ( Partial_Sums ( R_EAL seq)) = ( R_EAL ( Partial_Sums seq))

    proof

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

      

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

      proof

        let k be Nat;

        assume P[k];

        

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

        .= ((( Partial_Sums seq) . k) + (seq . (k + 1)));

        hence thesis by SERIES_1:def 1;

      end;

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

      then

       A2: P[ 0 ] by SERIES_1:def 1;

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

      hence thesis;

    end;

    theorem :: MESFUN9C:6

    

     Th6: (for x be Element of X st x in E holds (F # x) is summable) implies for x be Element of X st x in E holds ((F || E) # x) is summable

    proof

      set G = (F || E);

      assume

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

      let x be Element of X;

      assume

       A2: x in E;

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

      proof

        let n be Element of NAT ;

        ((F # x) . n) = ((F . n) . x) by SEQFUNC:def 10;

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

        then ((F # x) . n) = ((G . n) . x) by Def1;

        hence ((F # x) . n) = ((G # x) . n) by SEQFUNC:def 10;

      end;

      then

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

      (F # x) is summable by A1, A2;

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

      hence (G # x) is summable by A3;

    end;

    definition

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

      :: MESFUN9C:def2

      func Partial_Sums F -> Functional_Sequence of X, REAL means

      : Def2: (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, REAL & $3 = (F . $1)) or ($2 is PartFunc of X, REAL & for F2 be PartFunc of X, REAL 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;

          now

            assume x is PartFunc of X, REAL ;

            then

            reconsider G2 = x as PartFunc of X, REAL ;

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

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

          end;

          hence thesis;

        end;

        consider IT be Function such that

         A2: ( 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, REAL ;

          let f be object;

          assume f in ( rng IT);

          then

          consider m be object such that

           A3: m in ( dom IT) and

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

          reconsider m as Element of NAT by A2, A3;

          

           A5: 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, REAL ;

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

            hence IND[(n + 1)];

          end;

          

           A6: IND[ 0 ] by A2;

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

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

          hence f in ( PFuncs (X, REAL )) by A4, PARTFUN1: 45;

        end;

        then ( rng IT) c= ( PFuncs (X, REAL )) by TARSKI:def 3;

        then

        reconsider IT as Functional_Sequence of X, REAL by A2, FUNCT_2:def 1, RELSET_1: 4;

        take IT;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let PS1,PS2 be Functional_Sequence of X, REAL ;

        assume that

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

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

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

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

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

        

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

        proof

          let n be Nat;

          assume

           A12: IND[n];

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

          hence (PS1 . (n + 1)) = (PS2 . (n + 1)) by A10, A12;

        end;

        

         A13: IND[ 0 ] by A7, A9;

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

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

        hence thesis;

      end;

    end

    theorem :: MESFUN9C:7

    

     Th7: ( Partial_Sums ( R_EAL F)) = ( R_EAL ( Partial_Sums F))

    proof

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

      

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

      proof

        let k be Nat;

        assume P[k];

        

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

        .= ( R_EAL ((( Partial_Sums F) . k) + (F . (k + 1)))) by MESFUNC6: 23;

        hence thesis by Def2;

      end;

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

      .= ( R_EAL (( Partial_Sums F) . 0 )) by Def2;

      then

       A2: P[ 0 ];

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

      hence thesis;

    end;

    theorem :: MESFUN9C:8

    

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

    proof

      (( Partial_Sums F) . n) = (( R_EAL ( Partial_Sums F)) . n);

      then

       A1: (( Partial_Sums F) . n) = (( Partial_Sums ( R_EAL F)) . n) by Th7;

      (( Partial_Sums ( R_EAL F)) . m) = (( R_EAL ( Partial_Sums F)) . m) by Th7;

      hence thesis by A1, MESFUNC9: 22;

    end;

    theorem :: MESFUN9C:9

    

     Th9: ( R_EAL F) is additive

    proof

      now

        let n,m be Nat;

        assume n <> m;

        let x be set;

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

        (( R_EAL F) . n) = ( R_EAL (F . n));

        hence ((( R_EAL F) . n) . x) <> +infty or ((( R_EAL F) . m) . x) <> -infty ;

      end;

      hence thesis by MESFUNC9:def 5;

    end;

    theorem :: MESFUN9C:10

    

     Th10: ( dom (( Partial_Sums F) . n)) = ( meet { ( dom (F . k)) where k be Element of NAT : k <= n })

    proof

      ( dom (( Partial_Sums ( R_EAL F)) . n)) = ( meet { ( dom (( R_EAL F) . k)) where k be Element of NAT : k <= n }) & (( Partial_Sums ( R_EAL F)) . n) = (( R_EAL ( Partial_Sums F)) . n) by Th7, Th9, MESFUNC9: 28;

      hence thesis;

    end;

    theorem :: MESFUN9C:11

    

     Th11: F is with_the_same_dom implies ( dom (( Partial_Sums F) . n)) = ( dom (F . 0 ))

    proof

      assume F is with_the_same_dom;

      then ( dom (( Partial_Sums ( R_EAL F)) . n)) = ( dom (( R_EAL F) . 0 )) by Th9, MESFUNC9: 29;

      then ( dom (( R_EAL ( Partial_Sums F)) . n)) = ( dom (( R_EAL F) . 0 )) by Th7;

      hence thesis;

    end;

    theorem :: MESFUN9C:12

    

     Th12: 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

      assume F is with_the_same_dom & D c= ( dom (F . 0 )) & x in D;

      then (( Partial_Sums (( R_EAL F) # x)) . n) = ((( Partial_Sums ( R_EAL F)) # x) . n) by Th9, MESFUNC9: 32;

      then (( Partial_Sums ( R_EAL (F # x))) . n) = ((( Partial_Sums ( R_EAL F)) # x) . n) by MESFUN7C: 1;

      then (( R_EAL ( Partial_Sums (F # x))) . n) = ((( Partial_Sums ( R_EAL F)) # x) . n) by Th5;

      then (( Partial_Sums (F # x)) . n) = ((( R_EAL ( Partial_Sums F)) # x) . n) by Th7;

      hence thesis by MESFUN7C: 1;

    end;

    theorem :: MESFUN9C:13

    

     Th13: F is with_the_same_dom & D c= ( dom (F . 0 )) & x in D implies (( Partial_Sums (F # x)) is convergent iff (( Partial_Sums F) # x) is convergent)

    proof

      assume

       A1: F is with_the_same_dom & D c= ( dom (F . 0 )) & x in D;

      

       A2: ( R_EAL (F # x)) = (( R_EAL F) # x) by MESFUN7C: 1;

      ( Partial_Sums ( R_EAL F)) = ( R_EAL ( Partial_Sums F)) by Th7;

      then

       A3: (( Partial_Sums ( R_EAL F)) # x) = (( Partial_Sums F) # x) by MESFUN7C: 1;

      

       A4: ( Partial_Sums (F # x)) = ( R_EAL ( Partial_Sums (F # x)))

      .= ( Partial_Sums ( R_EAL (F # x))) by Th5;

      

       A5: ( R_EAL F) is additive by Th9;

      hereby

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

        then ( Partial_Sums ( R_EAL (F # x))) is convergent_to_finite_number by A4, RINFSUP2: 14;

        then (( Partial_Sums ( R_EAL F)) # x) is convergent_to_finite_number by A1, A5, A2, MESFUNC9: 33;

        hence (( Partial_Sums F) # x) is convergent by A3, RINFSUP2: 15;

      end;

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

      then (( Partial_Sums ( R_EAL F)) # x) is convergent_to_finite_number by A3, RINFSUP2: 14;

      then ( Partial_Sums (( R_EAL F) # x)) is convergent_to_finite_number by A1, A5, MESFUNC9: 33;

      hence ( Partial_Sums (F # x)) is convergent by A4, A2, RINFSUP2: 15;

    end;

    theorem :: MESFUN9C:14

    

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

    proof

      assume that

       A1: F is with_the_same_dom & ( dom f) c= ( dom (F . 0 )) & x in ( dom f) and

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

      

       A3: ( dom ( Partial_Sums (F # x))) = NAT & ( dom (( Partial_Sums F) # x)) = NAT by FUNCT_2:def 1;

      for n be object st n in NAT holds (( Partial_Sums (F # x)) . n) = ((( Partial_Sums F) # x) . n) by A1, Th12;

      hence (f . x) = ( lim (( Partial_Sums F) # x)) by A2, A3, FUNCT_1: 2;

    end;

    theorem :: MESFUN9C:15

    

     Th15: (for m be Nat holds (F . m) is_simple_func_in S) implies (( Partial_Sums F) . n) is_simple_func_in S

    proof

      assume

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

      for m be Nat holds (( R_EAL F) . m) is_simple_func_in S

      proof

        let m be Nat;

        (F . m) is_simple_func_in S by A1;

        then ( R_EAL (F . m)) is_simple_func_in S by MESFUNC6: 49;

        hence (( R_EAL F) . m) is_simple_func_in S;

      end;

      then (( Partial_Sums ( R_EAL F)) . n) is_simple_func_in S by MESFUNC9: 35;

      then (( R_EAL ( Partial_Sums F)) . n) is_simple_func_in S by Th7;

      then ( R_EAL (( Partial_Sums F) . n)) is_simple_func_in S;

      hence (( Partial_Sums F) . n) is_simple_func_in S by MESFUNC6: 49;

    end;

    theorem :: MESFUN9C:16

    

     Th16: (for n be Nat holds (F . n) is E -measurable) 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;

      

       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 E -measurable by A1;

        then ((PF . k) + (F . (k + 1))) is E -measurable by A3, MESFUNC6: 26;

        hence thesis by Def2;

      end;

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

      then

       A4: P[ 0 ] by A1;

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

      hence (( Partial_Sums F) . m) is E -measurable;

    end;

    theorem :: MESFUN9C:17

    

     Th17: for X be non empty set, F be Functional_Sequence of X, REAL st 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, REAL ;

      assume

       A1: F is with_the_same_dom;

      let n,m be Nat;

      ( dom (( Partial_Sums F) . n)) = ( dom (F . 0 )) by A1, Th11;

      hence ( dom (( Partial_Sums F) . n)) = ( dom (( Partial_Sums F) . m)) by A1, Th11;

    end;

    theorem :: MESFUN9C:18

    

     Th18: ( dom (F . 0 )) = E & 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 & F is with_the_same_dom and

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

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

       A4:

      now

        let x be Element of X;

        assume

         A5: x in E;

        then (F # x) is summable by A3;

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

        hence (( Partial_Sums F) # x) is convergent by A1, A5, Th13;

      end;

      ( dom (( Partial_Sums F) . 0 )) = E & ( Partial_Sums F) is with_the_same_dom Functional_Sequence of X, REAL by A1, Th11, Th17;

      hence thesis by A2, A4, MESFUN7C: 21;

    end;

    theorem :: MESFUN9C:19

    

     Th19: (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

      assume

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

      let m be Nat;

      for n be Nat holds (( R_EAL F) . n) is_integrable_on M

      proof

        let n be Nat;

        (F . n) is_integrable_on M by A1;

        then ( R_EAL (F . n)) is_integrable_on M;

        hence (( R_EAL F) . n) is_integrable_on M;

      end;

      then (( Partial_Sums ( R_EAL F)) . m) is_integrable_on M by MESFUNC9: 45;

      then (( R_EAL ( Partial_Sums F)) . m) is_integrable_on M by Th7;

      then ( R_EAL (( Partial_Sums F) . m)) is_integrable_on M;

      hence (( Partial_Sums F) . m) is_integrable_on M;

    end;

    begin

    reserve F for Functional_Sequence of X, COMPLEX ,

f for PartFunc of X, COMPLEX ,

A for set;

    theorem :: MESFUN9C:20

    

     Th20: (( Re f) | A) = ( Re (f | A)) & (( Im f) | A) = ( Im (f | A))

    proof

      ( dom (( Re f) | A)) = (( dom ( Re f)) /\ A) by RELAT_1: 61

      .= (( dom f) /\ A) by COMSEQ_3:def 3;

      

      then

       A1: ( dom (( Re f) | A)) = ( dom (f | A)) by RELAT_1: 61

      .= ( dom ( Re (f | A))) by COMSEQ_3:def 3;

      now

        let x be object;

        assume

         A2: x in ( dom (( Re f) | A));

        then

         A3: x in (( dom ( Re f)) /\ A) by RELAT_1: 61;

        then

         A4: x in ( dom ( Re f)) by XBOOLE_0:def 4;

        

         A5: x in A by A3, XBOOLE_0:def 4;

        

        thus (( Re (f | A)) . x) = ( Re ((f | A) . x)) by A1, A2, COMSEQ_3:def 3

        .= ( Re (f . x)) by A5, FUNCT_1: 49

        .= (( Re f) . x) by A4, COMSEQ_3:def 3

        .= ((( Re f) | A) . x) by A5, FUNCT_1: 49;

      end;

      hence (( Re f) | A) = ( Re (f | A)) by A1, FUNCT_1: 2;

      ( dom (( Im f) | A)) = (( dom ( Im f)) /\ A) by RELAT_1: 61;

      then ( dom (( Im f) | A)) = (( dom f) /\ A) by COMSEQ_3:def 4;

      

      then

       A6: ( dom (( Im f) | A)) = ( dom (f | A)) by RELAT_1: 61

      .= ( dom ( Im (f | A))) by COMSEQ_3:def 4;

      now

        let x be object;

        assume

         A7: x in ( dom (( Im f) | A));

        then

         A8: x in (( dom ( Im f)) /\ A) by RELAT_1: 61;

        then

         A9: x in ( dom ( Im f)) by XBOOLE_0:def 4;

        

         A10: x in A by A8, XBOOLE_0:def 4;

        

        thus (( Im (f | A)) . x) = ( Im ((f | A) . x)) by A6, A7, COMSEQ_3:def 4

        .= ( Im (f . x)) by A10, FUNCT_1: 49

        .= (( Im f) . x) by A9, COMSEQ_3:def 4

        .= ((( Im f) | A) . x) by A10, FUNCT_1: 49;

      end;

      hence (( Im f) | A) = ( Im (f | A)) by A6, FUNCT_1: 2;

    end;

    

     Lm1: for n be Nat holds (( Re (F || D)) . n) = ((( Re F) . n) | D) & (( Im (F || D)) . n) = ((( Im F) . n) | D)

    proof

      set G = (F || D);

      let n be Nat;

      ( Re ((F . n) | D)) = (( Re (F . n)) | D) by Th20;

      then

       A1: ( Re ((F . n) | D)) = ((( Re F) . n) | D) by MESFUN7C: 24;

      ( Im ((F . n) | D)) = (( Im (F . n)) | D) by Th20;

      then

       A2: ( Im ((F . n) | D)) = ((( Im F) . n) | D) by MESFUN7C: 24;

      ( Re (G . n)) = (( Re G) . n) & ( Im (G . n)) = (( Im G) . n) by MESFUN7C: 24;

      hence (( Re G) . n) = ((( Re F) . n) | D) & (( Im G) . n) = ((( Im F) . n) | D) by A1, A2, Def1;

    end;

    theorem :: MESFUN9C:21

    

     Th21: ( Re (F || D)) = (( Re F) || D)

    proof

      let n be Element of NAT ;

      (( Re (F || D)) . n) = ((( Re F) . n) | D) by Lm1;

      hence thesis by Def1;

    end;

    theorem :: MESFUN9C:22

    

     Th22: ( Im (F || D)) = (( Im F) || D)

    proof

      let n be Element of NAT ;

      (( Im (F || D)) . n) = ((( Im F) . n) | D) by Lm1;

      hence thesis by Def1;

    end;

    theorem :: MESFUN9C:23

    

     Th23: F is with_the_same_dom & D c= ( dom (F . 0 )) & x in D implies ((F # x) is convergent implies ((F || D) # x) is convergent)

    proof

      set G = (F || D);

      assume that

       A1: F is with_the_same_dom and

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

       A3: x in D;

      ( Re G) = (( Re F) || D) by Th21;

      then

       A4: (( Re F) # x) is convergent implies (( Re G) # x) is convergent by A3, Th1;

      ( dom (( Re F) . 0 )) = ( dom (F . 0 )) by MESFUN7C:def 11;

      then ( dom ((( Re F) . 0 ) | D)) = D by A2, RELAT_1: 62;

      then ( dom (( Re G) . 0 )) = D by Lm1;

      then

       A5: ( dom (G . 0 )) = D by MESFUN7C:def 11;

      G is with_the_same_dom by A1, Th2;

      then

       A6: (( Re G) # x) = ( Re (G # x)) & (( Im G) # x) = ( Im (G # x)) by A3, A5, MESFUN7C: 23;

      ( Im G) = (( Im F) || D) by Th22;

      then

       A7: (( Im F) # x) is convergent implies (( Im G) # x) is convergent by A3, Th1;

      (( Re F) # x) = ( Re (F # x)) & (( Im F) # x) = ( Im (F # x)) by A1, A2, A3, MESFUN7C: 23;

      hence thesis by A4, A7, A6, COMSEQ_3: 42;

    end;

    theorem :: MESFUN9C:24

    

     Th24: F is with_the_same_dom iff ( Re F) is with_the_same_dom

    proof

      thus F is with_the_same_dom implies ( Re F) is with_the_same_dom;

      assume

       A1: ( Re F) is with_the_same_dom;

      now

        let n,m be Nat;

        ( dom (( Re F) . n)) = ( dom (F . n)) & ( dom (( Re F) . m)) = ( dom (F . m)) by MESFUN7C:def 11;

        hence ( dom (F . n)) = ( dom (F . m)) by A1;

      end;

      hence F is with_the_same_dom;

    end;

    theorem :: MESFUN9C:25

    

     Th25: ( Re F) is with_the_same_dom iff ( Im F) is with_the_same_dom

    proof

      hereby

        assume ( Re F) is with_the_same_dom;

        then F is with_the_same_dom by Th24;

        then for n,m be Nat holds ( dom (( Im F) . n)) = ( dom (( Im F) . m)) by MESFUN7C:def 12, MESFUNC8:def 2;

        hence ( Im F) is with_the_same_dom;

      end;

      assume

       A1: ( Im F) is with_the_same_dom;

      now

        let n,m be Nat;

        ( dom (( Im F) . n)) = ( dom (F . n)) & ( dom (( Im F) . m)) = ( dom (F . m)) by MESFUN7C:def 12;

        hence ( dom (F . n)) = ( dom (F . m)) by A1;

      end;

      then F is with_the_same_dom;

      hence ( Re F) is with_the_same_dom;

    end;

    theorem :: MESFUN9C:26

    F is with_the_same_dom & D = ( dom (F . 0 )) & (for x be Element of X st x in D holds (F # x) is convergent) implies (( lim F) | D) = ( lim (F || D))

    proof

      set G = (F || D);

      assume that

       A1: F is with_the_same_dom and

       A2: D = ( dom (F . 0 )) and

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

      

       A4: ( Re G) = (( Re F) || D) by Th21;

       A5:

      now

        let x be Element of X;

        ( dom ((F . 0 ) | D)) = D by A2, RELAT_1: 62;

        then

         A6: ( dom (G . 0 )) = D by Def1;

        assume

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

        then (F # x) is convergent by A3, A6;

        hence (G # x) is convergent by A1, A2, A7, A6, Th23;

      end;

      

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

      proof

        let x be Element of X;

        assume

         A9: x in D;

        then (F # x) is convergent Complex_Sequence by A3;

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

        hence (( Re F) # x) is convergent by A1, A2, A9, MESFUN7C: 23;

      end;

      D c= ( dom (( Re F) . 0 )) by A2, MESFUN7C:def 11;

      then (( lim ( Re F)) | D) = ( lim ( Re G)) by A4, A8, Th3;

      then

       A10: (( Re ( lim F)) | D) = ( lim ( Re G)) by A1, A2, A3, MESFUN7C: 25;

      

       A11: G is with_the_same_dom by A1, Th2;

      then ( lim ( Re G)) = ( Re ( lim G)) by A5, MESFUN7C: 25;

      then

       A12: ( Re (( lim F) | D)) = ( Re ( lim G)) by A10, Th20;

      

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

      proof

        let x be Element of X;

        assume

         A14: x in D;

        then (F # x) is convergent Complex_Sequence by A3;

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

        hence (( Im F) # x) is convergent by A1, A2, A14, MESFUN7C: 23;

      end;

      

       A15: ( Im G) = (( Im F) || D) by Th22;

      D c= ( dom (( Im F) . 0 )) by A2, MESFUN7C:def 12;

      then (( lim ( Im F)) | D) = ( lim ( Im G)) by A15, A13, Th3;

      then

       A16: (( Im ( lim F)) | D) = ( lim ( Im G)) by A1, A2, A3, MESFUN7C: 25;

      ( lim ( Im G)) = ( Im ( lim G)) by A11, A5, MESFUN7C: 25;

      then

       A17: ( Im (( lim F) | D)) = ( Im ( lim G)) by A16, Th20;

      

      thus ( lim G) = (( Re ( lim G)) + ( <i> (#) ( Im ( lim G)))) by MESFUN6C: 8

      .= (( lim F) | D) by A12, A17, MESFUN6C: 8;

    end;

    theorem :: MESFUN9C:27

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

    proof

      set G = (F || E);

      

       A1: ( Re G) = (( Re F) || E) by Th21;

      

       A2: ( Im G) = (( Im F) || E) by Th22;

      assume F is with_the_same_dom;

      then

       A3: ( Re F) is with_the_same_dom;

      then

       A4: ( Im F) is with_the_same_dom by Th25;

      assume

       A5: E c= ( dom (F . 0 ));

      assume

       A6: for m be Nat holds (F . m) is E -measurable;

      

       A7: for m be Nat holds (( Re F) . m) is E -measurable & (( Im F) . m) is E -measurable

      proof

        let m be Nat;

        (F . m) is E -measurable by A6;

        then ( Re (F . m)) is E -measurable & ( Im (F . m)) is E -measurable by MESFUN6C:def 1;

        hence thesis by MESFUN7C: 24;

      end;

      E c= ( dom (( Im F) . 0 )) by A5, MESFUN7C:def 12;

      then (( Im G) . n) is E -measurable by A4, A2, A7, Th4;

      then

       A8: ( Im (G . n)) is E -measurable by MESFUN7C: 24;

      E c= ( dom (( Re F) . 0 )) by A5, MESFUN7C:def 11;

      then (( Re G) . n) is E -measurable by A3, A1, A7, Th4;

      then ( Re (G . n)) is E -measurable by MESFUN7C: 24;

      hence thesis by A8, MESFUN6C:def 1;

    end;

    theorem :: MESFUN9C:28

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

    proof

      set G = (F || E);

      assume that

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

       A2: F is with_the_same_dom and

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

      

       A4: G is with_the_same_dom by A2, Th2;

      

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

      proof

        let x be Element of X;

        assume

         A6: x in E;

        then (F # x) is summable by A3;

        then ( Im (F # x)) is summable;

        hence (( Im F) # x) is summable by A1, A2, A6, MESFUN7C: 23;

      end;

      

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

      proof

        let x be Element of X;

        assume

         A8: x in E;

        then (F # x) is summable by A3;

        then ( Re (F # x)) is summable;

        hence (( Re F) # x) is summable by A1, A2, A8, MESFUN7C: 23;

      end;

      hereby

        let x be Element of X;

        assume

         A9: x in E;

        (G . 0 ) = ((F . 0 ) | E) by Def1;

        then

         A10: x in ( dom (G . 0 )) by A1, A9, RELAT_1: 62;

        ( Im G) = (( Im F) || E) by Th22;

        then (( Im G) # x) is summable by A5, A9, Th6;

        then

         A11: ( Im (G # x)) is summable by A4, A10, MESFUN7C: 23;

        ( Re G) = (( Re F) || E) by Th21;

        then (( Re G) # x) is summable by A7, A9, Th6;

        then ( Re (G # x)) is summable by A4, A10, MESFUN7C: 23;

        hence (G # x) is summable by A11, COMSEQ_3: 57;

      end;

    end;

    definition

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

      :: MESFUN9C:def3

      func Partial_Sums F -> Functional_Sequence of X, COMPLEX means

      : Def3: (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, COMPLEX & $3 = (F . $1)) or ($2 is PartFunc of X, COMPLEX & for F2 be PartFunc of X, COMPLEX st F2 = $2 holds $3 = (F2 + (F . ($1 + 1))));

        

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

        proof

          let n be Nat;

          let x be set;

          now

            assume x is PartFunc of X, COMPLEX ;

            then

            reconsider G2 = x as PartFunc of X, COMPLEX ;

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

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

          end;

          hence thesis;

        end;

        consider IT be Function such that

         A2: ( 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, COMPLEX ;

          let f be object;

          assume f in ( rng IT);

          then

          consider m be object such that

           A3: m in ( dom IT) and

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

          reconsider m as Element of NAT by A2, A3;

          

           A5: 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, COMPLEX ;

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

            hence IND[(n + 1)];

          end;

          

           A6: IND[ 0 ] by A2;

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

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

          hence f in ( PFuncs (X, COMPLEX )) by A4, PARTFUN1: 45;

        end;

        then ( rng IT) c= ( PFuncs (X, COMPLEX )) by TARSKI:def 3;

        then

        reconsider IT as Functional_Sequence of X, COMPLEX by A2, FUNCT_2:def 1, RELSET_1: 4;

        take IT;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let PS1,PS2 be Functional_Sequence of X, COMPLEX ;

        assume that

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

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

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

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

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

        

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

        proof

          let n be Nat;

          assume

           A12: IND[n];

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

          hence (PS1 . (n + 1)) = (PS2 . (n + 1)) by A10, A12;

        end;

        

         A13: IND[ 0 ] by A7, A9;

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

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

        hence thesis;

      end;

    end

    theorem :: MESFUN9C:29

    

     Th29: ( Partial_Sums ( Re F)) = ( Re ( Partial_Sums F)) & ( Partial_Sums ( Im F)) = ( Im ( Partial_Sums F))

    proof

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

      defpred R[ Nat] means (( Partial_Sums ( Im F)) . $1) = (( Im ( Partial_Sums F)) . $1);

      

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

      proof

        let k be Nat;

        assume P[k];

        

        then (( Partial_Sums ( Re F)) . (k + 1)) = ((( Re ( Partial_Sums F)) . k) + (( Re F) . (k + 1))) by Def2

        .= ((( Re ( Partial_Sums F)) . k) + ( Re (F . (k + 1)))) by MESFUN7C: 24

        .= (( Re (( Partial_Sums F) . k)) + ( Re (F . (k + 1)))) by MESFUN7C: 24

        .= ( Re ((( Partial_Sums F) . k) + (F . (k + 1)))) by MESFUN6C: 5

        .= ( Re (( Partial_Sums F) . (k + 1))) by Def3;

        hence thesis by MESFUN7C: 24;

      end;

      

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

      proof

        let k be Nat;

        assume R[k];

        

        then (( Partial_Sums ( Im F)) . (k + 1)) = ((( Im ( Partial_Sums F)) . k) + (( Im F) . (k + 1))) by Def2

        .= ((( Im ( Partial_Sums F)) . k) + ( Im (F . (k + 1)))) by MESFUN7C: 24

        .= (( Im (( Partial_Sums F) . k)) + ( Im (F . (k + 1)))) by MESFUN7C: 24

        .= ( Im ((( Partial_Sums F) . k) + (F . (k + 1)))) by MESFUN6C: 5

        .= ( Im (( Partial_Sums F) . (k + 1))) by Def3;

        hence thesis by MESFUN7C: 24;

      end;

      (( Partial_Sums ( Im F)) . 0 ) = (( Im F) . 0 ) by Def2

      .= ( Im (F . 0 )) by MESFUN7C: 24

      .= ( Im (( Partial_Sums F) . 0 )) by Def3;

      then

       A3: R[ 0 ] by MESFUN7C: 24;

      

       A4: for i be Nat holds R[i] from NAT_1:sch 2( A3, A2);

      (( Partial_Sums ( Re F)) . 0 ) = (( Re F) . 0 ) by Def2

      .= ( Re (F . 0 )) by MESFUN7C: 24

      .= ( Re (( Partial_Sums F) . 0 )) by Def3;

      then

       A5: P[ 0 ] by MESFUN7C: 24;

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

      hence thesis by A4;

    end;

    theorem :: MESFUN9C:30

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

    proof

      assume

       A1: z in ( dom (( Partial_Sums F) . n)) & m <= n;

      

       A2: ( dom (( Partial_Sums F) . n)) = ( dom (( Re ( Partial_Sums F)) . n)) by MESFUN7C:def 11

      .= ( dom (( Partial_Sums ( Re F)) . n)) by Th29;

      ( dom (( Partial_Sums ( Re F)) . m)) = ( dom (( Re ( Partial_Sums F)) . m)) by Th29

      .= ( dom (( Partial_Sums F) . m)) by MESFUN7C:def 11;

      hence z in ( dom (( Partial_Sums F) . m)) by A1, A2, Th8;

      z in ( dom (( Re F) . m)) by A1, A2, Th8;

      hence z in ( dom (F . m)) by MESFUN7C:def 11;

    end;

    theorem :: MESFUN9C:31

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

    proof

      now

        let A be object;

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

        then

        consider i be Element of NAT such that

         A1: A = ( dom (( Re F) . i)) and

         A2: i <= n;

        A = ( dom (F . i)) by A1, MESFUN7C:def 11;

        hence A in { ( dom (F . k)) where k be Element of NAT : k <= n } by A2;

      end;

      then

       A3: { ( dom (( Re F) . k)) where k be Element of NAT : k <= n } c= { ( dom (F . k)) where k be Element of NAT : k <= n } by TARSKI:def 3;

      now

        let A be object;

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

        then

        consider i be Element of NAT such that

         A4: A = ( dom (F . i)) and

         A5: i <= n;

        A = ( dom (( Re F) . i)) by A4, MESFUN7C:def 11;

        hence A in { ( dom (( Re F) . k)) where k be Element of NAT : k <= n } by A5;

      end;

      then

       A6: { ( dom (F . k)) where k be Element of NAT : k <= n } c= { ( dom (( Re F) . k)) where k be Element of NAT : k <= n } by TARSKI:def 3;

      ( dom (( Partial_Sums ( Re F)) . n)) = ( dom (( Re ( Partial_Sums F)) . n)) by Th29;

      then

       A7: ( dom (( Partial_Sums ( Re F)) . n)) = ( dom (( Partial_Sums F) . n)) by MESFUN7C:def 11;

      ( dom (( Partial_Sums ( Re F)) . n)) = ( meet { ( dom (( Re F) . k)) where k be Element of NAT : k <= n }) by Th10;

      hence thesis by A7, A3, A6, XBOOLE_0:def 10;

    end;

    theorem :: MESFUN9C:32

    

     Th32: F is with_the_same_dom implies ( dom (( Partial_Sums F) . n)) = ( dom (F . 0 ))

    proof

      assume F is with_the_same_dom;

      then ( Re F) is with_the_same_dom;

      then ( dom (( Partial_Sums ( Re F)) . n)) = ( dom (( Re F) . 0 )) by Th11;

      then ( dom (( Partial_Sums ( Re F)) . n)) = ( dom (F . 0 )) by MESFUN7C:def 11;

      then ( dom (( Re ( Partial_Sums F)) . n)) = ( dom (F . 0 )) by Th29;

      hence ( dom (( Partial_Sums F) . n)) = ( dom (F . 0 )) by MESFUN7C:def 11;

    end;

    theorem :: MESFUN9C:33

    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

      assume that

       A1: F is with_the_same_dom and

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

       A3: x in D;

      

       A4: D c= ( dom (( Im F) . 0 )) by A2, MESFUN7C:def 12;

      ( dom (( Partial_Sums F) . n)) = ( dom (F . 0 )) by A1, Th32;

      then

       A5: x in ( dom (( Partial_Sums F) . n)) by A2, A3;

      then

       A6: x in ( dom ( Re (( Partial_Sums F) . n))) by COMSEQ_3:def 3;

      

       A7: ( Re F) is with_the_same_dom by A1;

      then ( Im F) is with_the_same_dom by Th25;

      then

       A8: (( Partial_Sums (( Im F) # x)) . n) = ((( Partial_Sums ( Im F)) # x) . n) by A3, A4, Th12;

      D c= ( dom (( Re F) . 0 )) by A2, MESFUN7C:def 11;

      then

       A9: (( Partial_Sums (( Re F) # x)) . n) = ((( Partial_Sums ( Re F)) # x) . n) by A3, A7, Th12;

      

       A10: ( Re (( Partial_Sums (F # x)) . n)) = (( Re ( Partial_Sums (F # x))) . n) by COMSEQ_3:def 5

      .= (( Partial_Sums ( Re (F # x))) . n) by COMSEQ_3: 26

      .= (( Partial_Sums (( Re F) # x)) . n) by A1, A2, A3, MESFUN7C: 23

      .= ((( Partial_Sums ( Re F)) . n) . x) by A9, SEQFUNC:def 10

      .= ((( Re ( Partial_Sums F)) . n) . x) by Th29

      .= (( Re (( Partial_Sums F) . n)) . x) by MESFUN7C: 24

      .= ( Re ((( Partial_Sums F) . n) . x)) by A6, COMSEQ_3:def 3

      .= ( Re ((( Partial_Sums F) # x) . n)) by MESFUN7C:def 9;

      

       A11: x in ( dom ( Im (( Partial_Sums F) . n))) by A5, COMSEQ_3:def 4;

      

       A12: ( Im (( Partial_Sums (F # x)) . n)) = (( Im ( Partial_Sums (F # x))) . n) by COMSEQ_3:def 6

      .= (( Partial_Sums ( Im (F # x))) . n) by COMSEQ_3: 26

      .= (( Partial_Sums (( Im F) # x)) . n) by A1, A2, A3, MESFUN7C: 23

      .= ((( Partial_Sums ( Im F)) . n) . x) by A8, SEQFUNC:def 10

      .= ((( Im ( Partial_Sums F)) . n) . x) by Th29

      .= (( Im (( Partial_Sums F) . n)) . x) by MESFUN7C: 24

      .= ( Im ((( Partial_Sums F) . n) . x)) by A11, COMSEQ_3:def 4

      .= ( Im ((( Partial_Sums F) # x) . n)) by MESFUN7C:def 9;

      

      thus (( Partial_Sums (F # x)) . n) = (( Re (( Partial_Sums (F # x)) . n)) + (( Im (( Partial_Sums (F # x)) . n)) * <i> )) by COMPLEX1: 13

      .= ((( Partial_Sums F) # x) . n) by A10, A12, COMPLEX1: 13;

    end;

    theorem :: MESFUN9C:34

    

     Th34: F is with_the_same_dom implies ( Partial_Sums F) is with_the_same_dom

    proof

      assume F is with_the_same_dom;

      then ( Re F) is with_the_same_dom;

      then ( Partial_Sums ( Re F)) is with_the_same_dom by Th17;

      then ( Re ( Partial_Sums F)) is with_the_same_dom by Th29;

      hence ( Partial_Sums F) is with_the_same_dom by Th24;

    end;

    theorem :: MESFUN9C:35

    

     Th35: F is with_the_same_dom & D c= ( dom (F . 0 )) & x in D implies (( Partial_Sums (F # x)) is convergent iff (( Partial_Sums F) # x) is convergent)

    proof

      assume that

       A1: F is with_the_same_dom and

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

       A3: x in D;

      

       A4: D c= ( dom (( Re F) . 0 )) by A2, MESFUN7C:def 11;

      

       A5: D c= ( dom (( Im F) . 0 )) by A2, MESFUN7C:def 12;

      

       A6: ( dom (( Partial_Sums F) . 0 )) = ( dom (F . 0 )) & ( Partial_Sums F) is with_the_same_dom by A1, Th32, Th34;

      

       A7: ( Re F) is with_the_same_dom by A1;

      then

       A8: ( Im F) is with_the_same_dom by Th25;

      hereby

        assume

         A9: ( Partial_Sums (F # x)) is convergent;

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

        then ( Partial_Sums ( Im (F # x))) is convergent by COMSEQ_3: 26;

        then ( Partial_Sums (( Im F) # x)) is convergent by A1, A2, A3, MESFUN7C: 23;

        then (( Partial_Sums ( Im F)) # x) is convergent by A3, A8, A5, Th13;

        then (( Im ( Partial_Sums F)) # x) is convergent by Th29;

        then

         A10: ( Im (( Partial_Sums F) # x)) is convergent by A2, A3, A6, MESFUN7C: 23;

        ( Re ( Partial_Sums (F # x))) is convergent by A9;

        then ( Partial_Sums ( Re (F # x))) is convergent by COMSEQ_3: 26;

        then ( Partial_Sums (( Re F) # x)) is convergent by A1, A2, A3, MESFUN7C: 23;

        then (( Partial_Sums ( Re F)) # x) is convergent by A3, A7, A4, Th13;

        then (( Re ( Partial_Sums F)) # x) is convergent by Th29;

        then ( Re (( Partial_Sums F) # x)) is convergent by A2, A3, A6, MESFUN7C: 23;

        hence (( Partial_Sums F) # x) is convergent by A10, COMSEQ_3: 42;

      end;

      assume

       A11: (( Partial_Sums F) # x) is convergent;

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

      then

       A12: (( Im ( Partial_Sums F)) # x) is convergent by A2, A3, A6, MESFUN7C: 23;

      

       A13: (( Im F) # x) = ( Im (F # x)) by A1, A2, A3, MESFUN7C: 23;

      ( Re (( Partial_Sums F) # x)) is convergent by A11;

      then

       A14: (( Re ( Partial_Sums F)) # x) is convergent by A2, A3, A6, MESFUN7C: 23;

      ( Partial_Sums (( Im F) # x)) is convergent iff (( Partial_Sums ( Im F)) # x) is convergent by A3, A8, A5, Th13;

      then

       A15: ( Im ( Partial_Sums (F # x))) is convergent by A12, A13, Th29, COMSEQ_3: 26;

      

       A16: (( Re F) # x) = ( Re (F # x)) by A1, A2, A3, MESFUN7C: 23;

      ( Partial_Sums (( Re F) # x)) is convergent iff (( Partial_Sums ( Re F)) # x) is convergent by A3, A7, A4, Th13;

      then ( Re ( Partial_Sums (F # x))) is convergent by A14, A16, Th29, COMSEQ_3: 26;

      hence ( Partial_Sums (F # x)) is convergent by A15, COMSEQ_3: 42;

    end;

    theorem :: MESFUN9C:36

    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

      assume that

       A1: F is with_the_same_dom and

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

       A3: x in ( dom f) and

       A4: (F # x) is summable and

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

      ( dom ( Re f)) = ( dom f) by COMSEQ_3:def 3;

      then

       A6: ( dom ( Re f)) c= ( dom (( Re F) . 0 )) by A2, MESFUN7C:def 11;

      ( Partial_Sums (F # x)) is convergent by A4;

      then (( Partial_Sums F) # x) is convergent by A1, A2, A3, Th35;

      then

       A7: ( lim ( Re (( Partial_Sums F) # x))) = ( Re ( lim (( Partial_Sums F) # x))) & ( lim ( Im (( Partial_Sums F) # x))) = ( Im ( lim (( Partial_Sums F) # x))) by COMSEQ_3: 41;

      ( dom ( Im f)) = ( dom f) by COMSEQ_3:def 4;

      then

       A8: ( dom ( Im f)) c= ( dom (( Im F) . 0 )) by A2, MESFUN7C:def 12;

      

       A9: x in ( dom ( Im f)) by A3, COMSEQ_3:def 4;

      then

       A10: (( Im f) . x) = ( Im (f . x)) by COMSEQ_3:def 4;

      

       A11: ( Partial_Sums F) is with_the_same_dom & ( dom (( Partial_Sums F) . 0 )) = ( dom (F . 0 )) by A1, Th32, Th34;

      then (( Re ( Partial_Sums F)) # x) = ( Re (( Partial_Sums F) # x)) by A2, A3, MESFUN7C: 23;

      then

       A12: ( lim (( Partial_Sums ( Re F)) # x)) = ( lim ( Re (( Partial_Sums F) # x))) by Th29;

      (( Im ( Partial_Sums F)) # x) = ( Im (( Partial_Sums F) # x)) by A2, A3, A11, MESFUN7C: 23;

      then

       A13: ( lim (( Partial_Sums ( Im F)) # x)) = ( lim ( Im (( Partial_Sums F) # x))) by Th29;

      

       A14: x in ( dom ( Re f)) by A3, COMSEQ_3:def 3;

      then

       A15: (( Re f) . x) = ( Re (f . x)) by COMSEQ_3:def 3;

      

       A16: ( Re F) is with_the_same_dom by A1;

      then

       A17: ( Im F) is with_the_same_dom by Th25;

      ( Re (F # x)) = (( Re F) # x) & ( Im (F # x)) = (( Im F) # x) by A1, A2, A3, MESFUN7C: 23;

      then

       A18: ( Sum (F # x)) = (( Sum (( Re F) # x)) + (( Sum (( Im F) # x)) * <i> )) by A4, COMSEQ_3: 53;

      then ( Re ( Sum (F # x))) = ( Sum (( Re F) # x)) by COMPLEX1: 12;

      then (( Re f) . x) = ( Sum (( Re F) # x)) by A5, A14, COMSEQ_3:def 3;

      then

       A19: (( Re f) . x) = ( lim (( Partial_Sums ( Re F)) # x)) by A16, A6, A14, Th14;

      ( Im ( Sum (F # x))) = ( Sum (( Im F) # x)) by A18, COMPLEX1: 12;

      then (( Im f) . x) = ( Sum (( Im F) # x)) by A5, A9, COMSEQ_3:def 4;

      then

       A20: (( Im f) . x) = ( lim (( Partial_Sums ( Im F)) # x)) by A17, A8, A9, Th14;

      

      thus (f . x) = (( Re (f . x)) + (( Im (f . x)) * <i> )) by COMPLEX1: 13

      .= ( lim (( Partial_Sums F) # x)) by A15, A10, A19, A20, A7, A12, A13, COMPLEX1: 13;

    end;

    theorem :: MESFUN9C:37

    (for m be Nat holds (F . m) is_simple_func_in S) implies (( Partial_Sums F) . n) is_simple_func_in S

    proof

      assume

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

      for m be Nat holds (( Im F) . m) is_simple_func_in S

      proof

        let m be Nat;

        (F . m) is_simple_func_in S by A1;

        then ( Im (F . m)) is_simple_func_in S by MESFUN7C: 43;

        hence (( Im F) . m) is_simple_func_in S by MESFUN7C: 24;

      end;

      then (( Partial_Sums ( Im F)) . n) is_simple_func_in S by Th15;

      then (( Im ( Partial_Sums F)) . n) is_simple_func_in S by Th29;

      then

       A2: ( Im (( Partial_Sums F) . n)) is_simple_func_in S by MESFUN7C: 24;

      for m be Nat holds (( Re F) . m) is_simple_func_in S

      proof

        let m be Nat;

        (F . m) is_simple_func_in S by A1;

        then ( Re (F . m)) is_simple_func_in S by MESFUN7C: 43;

        hence (( Re F) . m) is_simple_func_in S by MESFUN7C: 24;

      end;

      then (( Partial_Sums ( Re F)) . n) is_simple_func_in S by Th15;

      then (( Re ( Partial_Sums F)) . n) is_simple_func_in S by Th29;

      then ( Re (( Partial_Sums F) . n)) is_simple_func_in S by MESFUN7C: 24;

      hence (( Partial_Sums F) . n) is_simple_func_in S by A2, MESFUN7C: 43;

    end;

    

     Lm2: (for n be Nat holds (F . n) is E -measurable) implies (( Re F) . m) is E -measurable & (( Im F) . m) is E -measurable

    proof

      assume for n be Nat holds (F . n) is E -measurable;

      then (F . m) is E -measurable;

      then ( Re (F . m)) is E -measurable & ( Im (F . m)) is E -measurable by MESFUN6C:def 1;

      hence (( Re F) . m) is E -measurable & (( Im F) . m) is E -measurable by MESFUN7C: 24;

    end;

    theorem :: MESFUN9C:38

    (for n be Nat holds (F . n) is E -measurable) implies (( Partial_Sums F) . m) is E -measurable

    proof

      assume

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

      then for n be Nat holds (( Im F) . n) is E -measurable by Lm2;

      then (( Partial_Sums ( Im F)) . m) is E -measurable by Th16;

      then (( Im ( Partial_Sums F)) . m) is E -measurable by Th29;

      then

       A2: ( Im (( Partial_Sums F) . m)) is E -measurable by MESFUN7C: 24;

      for n be Nat holds (( Re F) . n) is E -measurable by A1, Lm2;

      then (( Partial_Sums ( Re F)) . m) is E -measurable by Th16;

      then (( Re ( Partial_Sums F)) . m) is E -measurable by Th29;

      then ( Re (( Partial_Sums F) . m)) is E -measurable by MESFUN7C: 24;

      hence (( Partial_Sums F) . m) is E -measurable by A2, MESFUN6C:def 1;

    end;

    theorem :: MESFUN9C:39

    ( dom (F . 0 )) = E & 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 with_the_same_dom and

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

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

      

       A5: ( dom (( Im F) . 0 )) = E by A1, MESFUN7C:def 12;

      

       A6: for x be Element of X st x in ( dom (( Partial_Sums F) . 0 )) holds (( Partial_Sums F) # x) is convergent

      proof

        let x be Element of X;

        assume

         A7: x in ( dom (( Partial_Sums F) . 0 ));

        

         A8: ( dom (( Partial_Sums F) . 0 )) = ( dom (F . 0 )) by A2, Th32;

        then (F # x) is summable by A1, A4, A7;

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

        hence (( Partial_Sums F) # x) is convergent by A2, A7, A8, Th35;

      end;

      

       A9: for n be Nat holds (( Partial_Sums ( Im F)) . n) is E -measurable

      proof

        let n be Nat;

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

        then ( Im (( Partial_Sums F) . n)) is E -measurable by MESFUN6C:def 1;

        then (( Im ( Partial_Sums F)) . n) is E -measurable by MESFUN7C: 24;

        hence (( Partial_Sums ( Im F)) . n) is E -measurable by Th29;

      end;

      

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

      proof

        let x be Element of X;

        assume

         A11: x in E;

        then (F # x) is summable by A4;

        then ( Im (F # x)) is summable;

        hence (( Im F) # x) is summable by A1, A2, A11, MESFUN7C: 23;

      end;

      

       A12: ( Re F) is with_the_same_dom by A2;

      then ( Im F) is with_the_same_dom by Th25;

      then ( lim ( Partial_Sums ( Im F))) is E -measurable by A5, A9, A10, Th18;

      then

       A13: ( lim ( Im ( Partial_Sums F))) is E -measurable by Th29;

      

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

      proof

        let x be Element of X;

        assume

         A15: x in E;

        then (F # x) is summable by A4;

        then ( Re (F # x)) is summable;

        hence (( Re F) # x) is summable by A1, A2, A15, MESFUN7C: 23;

      end;

      

       A16: for n be Nat holds (( Partial_Sums ( Re F)) . n) is E -measurable

      proof

        let n be Nat;

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

        then ( Re (( Partial_Sums F) . n)) is E -measurable by MESFUN6C:def 1;

        then (( Re ( Partial_Sums F)) . n) is E -measurable by MESFUN7C: 24;

        hence (( Partial_Sums ( Re F)) . n) is E -measurable by Th29;

      end;

      

       A17: ( Partial_Sums F) is with_the_same_dom by A2, Th34;

      then ( lim ( Im ( Partial_Sums F))) = ( R_EAL ( Im ( lim ( Partial_Sums F)))) by A6, MESFUN7C: 25;

      then

       A18: ( Im ( lim ( Partial_Sums F))) is E -measurable by A13;

      ( dom (( Re F) . 0 )) = E by A1, MESFUN7C:def 11;

      then ( lim ( Partial_Sums ( Re F))) is E -measurable by A12, A16, A14, Th18;

      then

       A19: ( lim ( Re ( Partial_Sums F))) is E -measurable by Th29;

      ( lim ( Re ( Partial_Sums F))) = ( R_EAL ( Re ( lim ( Partial_Sums F)))) by A6, A17, MESFUN7C: 25;

      then ( Re ( lim ( Partial_Sums F))) is E -measurable by A19;

      hence ( lim ( Partial_Sums F)) is E -measurable by A18, MESFUN6C:def 1;

    end;

    theorem :: MESFUN9C:40

    (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

      assume

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

      

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

      proof

        let n be Nat;

        (F . n) is_integrable_on M by A1;

        then ( Im (F . n)) is_integrable_on M by MESFUN6C:def 2;

        hence (( Im F) . n) is_integrable_on M by MESFUN7C: 24;

      end;

      

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

      proof

        let n be Nat;

        (F . n) is_integrable_on M by A1;

        then ( Re (F . n)) is_integrable_on M by MESFUN6C:def 2;

        hence (( Re F) . n) is_integrable_on M by MESFUN7C: 24;

      end;

      thus for m be Nat holds (( Partial_Sums F) . m) is_integrable_on M

      proof

        let m be Nat;

        (( Partial_Sums ( Im F)) . m) is_integrable_on M by A2, Th19;

        then (( Im ( Partial_Sums F)) . m) is_integrable_on M by Th29;

        then

         A4: ( Im (( Partial_Sums F) . m)) is_integrable_on M by MESFUN7C: 24;

        (( Partial_Sums ( Re F)) . m) is_integrable_on M by A3, Th19;

        then (( Re ( Partial_Sums F)) . m) is_integrable_on M by Th29;

        then ( Re (( Partial_Sums F) . m)) is_integrable_on M by MESFUN7C: 24;

        hence (( Partial_Sums F) . m) is_integrable_on M by A4, MESFUN6C:def 2;

      end;

    end;

    begin

    reserve f,g for PartFunc of X, COMPLEX ,

A for Element of S;

    theorem :: MESFUN9C:41

    f is_simple_func_in S implies f is A -measurable

    proof

      assume

       A1: f is_simple_func_in S;

      then ( Im f) is_simple_func_in S by MESFUN7C: 43;

      then

       A2: ( Im f) is A -measurable by MESFUNC6: 50;

      ( Re f) is_simple_func_in S by A1, MESFUN7C: 43;

      then ( Re f) is A -measurable by MESFUNC6: 50;

      hence f is A -measurable by A2, MESFUN6C:def 1;

    end;

    theorem :: MESFUN9C:42

    f is_simple_func_in S implies (f | A) is_simple_func_in S

    proof

      assume

       A1: f is_simple_func_in S;

      then ( Im f) is_simple_func_in S by MESFUN7C: 43;

      then ( R_EAL ( Im f)) is_simple_func_in S by MESFUNC6: 49;

      then ( R_EAL (( Im f) | A)) is_simple_func_in S by MESFUNC5: 34;

      then (( Im f) | A) is_simple_func_in S by MESFUNC6: 49;

      then

       A2: ( Im (f | A)) is_simple_func_in S by MESFUN6C: 7;

      ( Re f) is_simple_func_in S by A1, MESFUN7C: 43;

      then ( R_EAL ( Re f)) is_simple_func_in S by MESFUNC6: 49;

      then ( R_EAL (( Re f) | A)) is_simple_func_in S by MESFUNC5: 34;

      then (( Re f) | A) is_simple_func_in S by MESFUNC6: 49;

      then ( Re (f | A)) is_simple_func_in S by MESFUN6C: 7;

      hence (f | A) is_simple_func_in S by A2, MESFUN7C: 43;

    end;

    theorem :: MESFUN9C:43

    f is_simple_func_in S implies ( dom f) is Element of S by MESFUNC2: 31;

    theorem :: MESFUN9C:44

    f is_simple_func_in S & g is_simple_func_in S implies (f + g) is_simple_func_in S

    proof

      assume

       A1: f is_simple_func_in S & g is_simple_func_in S;

      then ( Im f) is_simple_func_in S & ( Im g) is_simple_func_in S by MESFUN7C: 43;

      then (( Im f) + ( Im g)) is_simple_func_in S by MESFUNC6: 72;

      then

       A2: ( Im (f + g)) is_simple_func_in S by MESFUN6C: 5;

      ( Re f) is_simple_func_in S & ( Re g) is_simple_func_in S by A1, MESFUN7C: 43;

      then (( Re f) + ( Re g)) is_simple_func_in S by MESFUNC6: 72;

      then ( Re (f + g)) is_simple_func_in S by MESFUN6C: 5;

      hence thesis by A2, MESFUN7C: 43;

    end;

    theorem :: MESFUN9C:45

    for c be Complex st f is_simple_func_in S holds (c (#) f) is_simple_func_in S

    proof

      let c be Complex;

      assume

       A1: f is_simple_func_in S;

      then

       A2: ( Re f) is_simple_func_in S by MESFUN7C: 43;

      then

       A3: (( Im c) (#) ( Re f)) is_simple_func_in S by MESFUNC6: 73;

      

       A4: ( Im f) is_simple_func_in S by A1, MESFUN7C: 43;

      then (( Im c) (#) ( Im f)) is_simple_func_in S by MESFUNC6: 73;

      then (( - 1) (#) (( Im c) (#) ( Im f))) is_simple_func_in S by MESFUNC6: 73;

      then

       A5: ( R_EAL ( - (( Im c) (#) ( Im f)))) is_simple_func_in S by MESFUNC6: 49;

      (( Re c) (#) ( Re f)) is_simple_func_in S by A2, MESFUNC6: 73;

      then ( R_EAL (( Re c) (#) ( Re f))) is_simple_func_in S by MESFUNC6: 49;

      then (( R_EAL (( Re c) (#) ( Re f))) + ( R_EAL ( - (( Im c) (#) ( Im f))))) is_simple_func_in S by A5, MESFUNC5: 38;

      then ( R_EAL ((( Re c) (#) ( Re f)) - (( Im c) (#) ( Im f)))) is_simple_func_in S by MESFUNC6: 23;

      then ((( Re c) (#) ( Re f)) - (( Im c) (#) ( Im f))) is_simple_func_in S by MESFUNC6: 49;

      then

       A6: ( Re (c (#) f)) is_simple_func_in S by MESFUN6C: 3;

      (( Re c) (#) ( Im f)) is_simple_func_in S by A4, MESFUNC6: 73;

      then ((( Im c) (#) ( Re f)) + (( Re c) (#) ( Im f))) is_simple_func_in S by A3, MESFUNC6: 72;

      then ( Im (c (#) f)) is_simple_func_in S by MESFUN6C: 3;

      hence thesis by A6, MESFUN7C: 43;

    end;

    begin

    reserve F for with_the_same_dom Functional_Sequence of X, ExtREAL ,

P for PartFunc of X, ExtREAL ;

    theorem :: MESFUN9C:46

    

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

    proof

      assume that

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

       A2: E = ( dom P) and

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

       A4: P is_integrable_on M and

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

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

      

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

      

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

      proof

        let x be Element of X, k be Nat;

        assume

         A9: x in E;

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

        then

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

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

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

        then ( - (P . x)) <= ((F . k) . x) & ((F . k) . x) <= (P . x) by EXTREAL1: 23;

        hence ( - (P . x)) <= ((F # x) . k) & ((F # x) . k) <= (P . x) by MESFUNC5:def 13;

      end;

       A11:

      now

        let x be Element of X;

        assume

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

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

        proof

          let k be Nat;

          

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

          ((F # x) . k) >= ( - (P . x)) by A7, A8, A12;

          hence (( superior_realsequence (F # x)) . k) >= ( - (P . x)) by A13, XXREAL_0: 2;

        end;

        then ( lim_sup (F # x)) >= ( - (P . x)) by MESFUN10: 4;

        then

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

        now

          let y be ExtReal;

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

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

          hence (P . x) >= y by A7, A8, A12;

        end;

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

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

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

        then

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

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

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

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

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

      end;

       A16:

      now

        let x be Element of X;

        assume

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

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

        then (F # x) is convergent by A6;

        hence (( lim F) . x) = (( lim_sup F) . x) by A17, MESFUNC8: 14;

      end;

      

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

      E = ( dom ( lim F)) by A1, MESFUNC8:def 9;

      then ( lim F) = ( lim_sup F) by A7, A16, PARTFUN1: 5;

      hence ( lim F) is_integrable_on M by A2, A4, A7, A18, A11, MESFUNC5: 102;

    end;

    reserve F for with_the_same_dom Functional_Sequence of X, REAL ,

f,P for PartFunc of X, REAL ;

    theorem :: MESFUN9C:47

    

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

    proof

      assume that

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

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

       A3: P is_integrable_on M and

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

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

      

       A6: for n be Nat holds (( R_EAL F) . n) is E -measurable

      proof

        let n be Nat;

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

        then ( R_EAL (F . n)) is E -measurable;

        hence (( R_EAL F) . n) is E -measurable;

      end;

      

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

      proof

        let x be Element of X;

        assume x in E;

        then

         A8: (F # x) is convergent by A5;

        (( R_EAL F) # x) = (F # x) by MESFUN7C: 1;

        hence (( R_EAL F) # x) is convergent by A8, RINFSUP2: 14;

      end;

      

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

      proof

        let x be Element of X, n be Nat;

        

         A10: ( R_EAL |.(F . n).|) = |.( R_EAL (F . n)).| by MESFUNC6: 1;

        assume x in E;

        hence ( |.(( R_EAL F) . n).| . x) <= (( R_EAL P) . x) by A4, A10;

      end;

      ( R_EAL P) is_integrable_on M by A3;

      hence ( lim F) is_integrable_on M by A1, A6, A9, A7, Th46;

    end;

    theorem :: MESFUN9C:48

    

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

    proof

      assume that

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

       A2: E = ( dom P) and

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

       A4: P is_integrable_on M and

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

      

       A6: ( R_EAL P) is_integrable_on M by A4;

      

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

      proof

        let x be Element of X, n be Nat;

        

         A8: ( R_EAL |.(F . n).|) = |.( R_EAL (F . n)).| by MESFUNC6: 1;

        assume x in E;

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

      end;

      

       A9: for n be Nat holds (( R_EAL F) . n) is E -measurable

      proof

        let n be Nat;

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

        then ( R_EAL (F . n)) is E -measurable;

        hence (( R_EAL F) . n) is E -measurable;

      end;

      now

        let x be object;

        assume

         A10: x in ( dom P);

        then x in ( dom |.(F . 0 ).|) by A1, A2, VALUED_1:def 11;

        then ( |.(F . 0 ).| . x) = |.((F . 0 ) . x) qua Complex.| by VALUED_1:def 11;

        then |.((F . 0 ) . x) qua Complex.| <= (P . x) by A2, A5, A10;

        hence 0 <= (P . x) by COMPLEX1: 46;

      end;

      then P is nonnegative by MESFUNC6: 52;

      then

      consider J be ExtREAL_sequence such that

       A11: for n be Nat holds (J . n) = ( Integral (M,(( R_EAL F) . n))) and ( lim_inf J) >= ( Integral (M,( lim_inf ( R_EAL F)))) and ( lim_sup J) <= ( Integral (M,( lim_sup ( R_EAL F)))) and

       A12: (for x be Element of X st x in E holds (( R_EAL F) # x) is convergent) implies J is convergent & ( lim J) = ( Integral (M,( lim ( R_EAL F)))) by A1, A2, A9, A6, A7, MESFUN10: 17;

      

       A13: ( Integral (M,( R_EAL P))) < +infty by A6, MESFUNC5: 96;

      for n be Nat holds |.(J . n).| < +infty

      proof

        let n be Nat;

        

         A14: E = ( dom (( R_EAL F) . n)) & (( R_EAL F) . n) is E -measurable by A1, A9, MESFUNC8:def 2;

         |.(( R_EAL F) . n).| is_integrable_on M by A1, A2, A9, A6, A7, MESFUN10: 16;

        then (( R_EAL F) . n) is_integrable_on M by A14, MESFUNC5: 100;

        then

         A15: |.( Integral (M,(( R_EAL F) . n))).| <= ( Integral (M, |.(( R_EAL F) . n).|)) by MESFUNC5: 101;

        for x be Element of X st x in ( dom (( R_EAL F) . n)) holds |.((( R_EAL F) . n) . x).| <= (( R_EAL P) . x)

        proof

          let x be Element of X;

          assume

           A16: x in ( dom (( R_EAL F) . n));

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

          then

           A17: ( |.(( R_EAL F) . n).| . x) <= (( R_EAL P) . x) by A7;

          x in ( dom |.(( R_EAL F) . n).|) by A16, MESFUNC1:def 10;

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

        end;

        then ( Integral (M, |.(( R_EAL F) . n).|)) <= ( Integral (M,( R_EAL P))) by A2, A6, A14, MESFUNC5: 102;

        then |.( Integral (M,(( R_EAL F) . n))).| <= ( Integral (M,( R_EAL P))) by A15, XXREAL_0: 2;

        then |.( Integral (M,(( R_EAL F) . n))).| < +infty by A13, XXREAL_0: 2;

        hence |.(J . n).| < +infty by A11;

      end;

      then for n be Element of NAT st n in ( dom J) holds |.(J . n).| < +infty ;

      then J is real-valued by MESFUNC2:def 1;

      then

      reconsider I = J as Real_Sequence by RINFSUP2: 6;

      (for x be Element of X st x in E holds (F # x) is convergent) implies J is convergent_to_finite_number & ( lim J) = ( Integral (M,( lim F)))

      proof

        assume

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

         A19:

        now

          let x be Element of X;

          assume x in E;

          then

           A20: (F # x) is convergent by A18;

          (F # x) = (( R_EAL F) # x) by MESFUN7C: 1;

          hence (( R_EAL F) # x) is convergent by A20, RINFSUP2: 14;

        end;

        ( lim F) is_integrable_on M by A1, A2, A3, A4, A5, A18, Th47;

        then

         A21: -infty < ( Integral (M,( lim F))) & ( Integral (M,( lim F))) < +infty by MESFUNC5: 96;

        J is convergent implies J is convergent_to_finite_number by A12, A19, A21, MESFUNC5:def 12;

        hence thesis by A12, A19;

      end;

      then

       A22: (for x be Element of X st x in E holds (F # x) is convergent) implies I is convergent & ( lim I) = ( Integral (M,( lim F))) by RINFSUP2: 15;

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

      hence thesis by A22;

    end;

    definition

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

      :: MESFUN9C:def4

      attr F is uniformly_bounded means ex K be Real st for n be Nat, x be Element of X st x in ( dom (F . 0 )) holds |.((F . n) . x) qua Complex.| <= K;

    end

    theorem :: MESFUN9C:49

    

     Th49: (M . E) < +infty & E = ( dom (F . 0 )) & (for n be Nat holds (F . n) is E -measurable) & F is uniformly_bounded & (for x be Element of X st x in E holds (F # x) is convergent) implies (for n be Nat holds (F . n) is_integrable_on M) & ( lim F) is_integrable_on M & ex I be ExtREAL_sequence st (for n be Nat holds (I . n) = ( Integral (M,(F . n)))) & I is convergent & ( lim I) = ( Integral (M,( lim F)))

    proof

      assume that

       A1: (M . E) < +infty & E = ( dom (F . 0 )) and

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

       A3: F is uniformly_bounded and

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

      consider K be Real such that

       A5: for n be Nat, x be Element of X st x in ( dom (F . 0 )) holds |.((F . n) . x) qua Complex.| <= K by A3;

      

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

      proof

        let x be Element of X;

        assume x in E;

        then

         A7: (F # x) is convergent by A4;

        (( R_EAL F) # x) = (F # x) by MESFUN7C: 1;

        hence (( R_EAL F) # x) is convergent by A7, RINFSUP2: 14;

      end;

      for n be Nat, x be set st x in ( dom (( R_EAL F) . 0 )) holds |.((( R_EAL F) . n) . x).| <= K

      proof

        let n be Nat, x be set;

        

         A8: |.((F . n) . x) qua Complex.| = |.((F . n) . x).| by MESFUNC6: 43;

        assume x in ( dom (( R_EAL F) . 0 ));

        hence |.((( R_EAL F) . n) . x).| <= K by A5, A8;

      end;

      then

       A9: ( R_EAL F) is uniformly_bounded by MESFUN10:def 1;

      

       A10: for n be Nat holds (( R_EAL F) . n) is E -measurable

      proof

        let n be Nat;

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

        then ( R_EAL (F . n)) is E -measurable;

        hence (( R_EAL F) . n) is E -measurable;

      end;

      then

      consider I be ExtREAL_sequence such that

       A11: for n be Nat holds (I . n) = ( Integral (M,(( R_EAL F) . n))) and

       A12: I is convergent & ( lim I) = ( Integral (M,( lim ( R_EAL F)))) by A1, A9, A6, MESFUN10: 19;

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

      hence thesis by A1, A10, A9, A6, A12, MESFUN10: 19;

    end;

    definition

      let X be set, F be Functional_Sequence of X, REAL , f be PartFunc of X, REAL ;

      :: MESFUN9C:def5

      pred F is_uniformly_convergent_to f means F is with_the_same_dom & ( dom (F . 0 )) = ( dom f) & for e be Real st e > 0 holds ex N be Nat st for n be Nat, x be Element of X st n >= N & x in ( dom (F . 0 )) holds |.(((F . n) . x) - (f . x)) qua Complex.| < e;

    end

    theorem :: MESFUN9C:50

    

     Th50: (M . E) < +infty & E = ( dom (F . 0 )) & (for n be Nat holds (F . n) is_integrable_on M) & F is_uniformly_convergent_to f implies f is_integrable_on M & ex I be ExtREAL_sequence st (for n be Nat holds (I . n) = ( Integral (M,(F . n)))) & I is convergent & ( lim I) = ( Integral (M,f))

    proof

      assume that

       A1: (M . E) < +infty & E = ( dom (F . 0 )) and

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

       A3: F is_uniformly_convergent_to f;

      

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

      proof

        let n be Nat;

        (F . n) is_integrable_on M by A2;

        then ( R_EAL (F . n)) is_integrable_on M;

        hence (( R_EAL F) . n) is_integrable_on M;

      end;

      

       A5: for e be Real st e > 0 holds ex N be Nat st for n be Nat, x be set st n >= N & x in ( dom (( R_EAL F) . 0 )) holds |.(((( R_EAL F) . n) . x) - (( R_EAL f) . x)).| < e

      proof

        let e be Real;

        assume e > 0 ;

        then

        consider N be Nat such that

         A6: for n be Nat, x be Element of X st n >= N & x in ( dom (F . 0 )) holds |.(((F . n) . x) - (f . x)) qua Complex.| < e by A3;

        now

          let n be Nat, x be set;

          assume n >= N & x in ( dom (( R_EAL F) . 0 ));

          then

           A7: |.(((F . n) . x) - (f . x)) qua Complex.| < e by A6;

           |.(((F . n) . x) - (f . x)) qua Complex.| = |.(((F . n) . x) - (f . x)).| by MESFUNC6: 43;

          hence |.(((( R_EAL F) . n) . x) - (( R_EAL f) . x)).| < e by A7;

        end;

        hence thesis;

      end;

      ( dom (( R_EAL F) . 0 )) = ( dom ( R_EAL f)) by A3;

      then

       A8: ( R_EAL F) is_uniformly_convergent_to ( R_EAL f) by A5, MESFUN10:def 2;

      then

       A9: ( R_EAL f) is_integrable_on M by A1, A4, MESFUN10: 21;

      consider I be ExtREAL_sequence such that

       A10: for n be Nat holds (I . n) = ( Integral (M,(( R_EAL F) . n))) and

       A11: I is convergent & ( lim I) = ( Integral (M,( R_EAL f))) by A1, A4, A8, MESFUN10: 21;

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

      hence thesis by A9, A11;

    end;

    reserve F for with_the_same_dom Functional_Sequence of X, COMPLEX ,

f for PartFunc of X, COMPLEX ;

    theorem :: MESFUN9C:51

    

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

    proof

      assume that

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

       A2: E = ( dom P) and

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

       A4: P is_integrable_on M and

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

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

      

       A7: for n be Nat holds (( Re F) . n) is E -measurable & (( Im F) . n) is E -measurable by A3, Lm2;

      for x be Element of X, n be Nat st x in E holds ( |.(( Re F) . n).| . x) <= (P . x) & ( |.(( Im F) . n).| . x) <= (P . x)

      proof

        let x be Element of X, n be Nat;

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

        ( Re ((F # x) . n1)) = (( Re (F # x)) . n1) by COMSEQ_3:def 5;

        then

         A8: |.(( Re (F # x)) . n) qua Complex.| <= |.((F # x) . n) qua Complex.| by COMSEQ_3: 13;

        ( Im ((F # x) . n1)) = (( Im (F # x)) . n1) by COMSEQ_3:def 6;

        then

         A9: |.(( Im (F # x)) . n) qua Complex.| <= |.((F # x) . n) qua Complex.| by COMSEQ_3: 13;

        assume

         A10: x in E;

        then ( |.(F . n).| . x) <= (P . x) by A5;

        then |.((F . n) . x).| <= (P . x) by VALUED_1: 18;

        then

         A11: |.((F # x) . n).| <= (P . x) by MESFUN7C:def 9;

        (( Im F) # x) = ( Im (F # x)) by A1, A10, MESFUN7C: 23;

        then |.((( Im F) # x) . n1) qua Complex.| <= (P . x) by A11, A9, XXREAL_0: 2;

        then

         A12: |.((( Im F) . n1) . x) qua Complex.| <= (P . x) by SEQFUNC:def 10;

        (( Re F) # x) = ( Re (F # x)) by A1, A10, MESFUN7C: 23;

        then |.((( Re F) # x) . n1) qua Complex.| <= (P . x) by A11, A8, XXREAL_0: 2;

        then |.((( Re F) . n1) . x) qua Complex.| <= (P . x) by SEQFUNC:def 10;

        hence ( |.(( Re F) . n).| . x) <= (P . x) & ( |.(( Im F) . n).| . x) <= (P . x) by A12, VALUED_1: 18;

      end;

      then

       A13: for x be Element of X, n be Nat holds (x in E implies ( |.(( Re F) . n).| . x) <= (P . x)) & (x in E implies ( |.(( Im F) . n).| . x) <= (P . x));

      

       A14: for x be Element of X st x in E holds (( Re F) # x) is convergent & (( Im F) # x) is convergent

      proof

        let x be Element of X;

        assume

         A15: x in E;

        then (F # x) is convergent Complex_Sequence by A6;

        then ( Re (F # x)) is convergent & ( Im (F # x)) is convergent;

        hence (( Re F) # x) is convergent & (( Im F) # x) is convergent by A1, A15, MESFUN7C: 23;

      end;

      then

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

      E = ( dom (( Im F) . 0 )) by A1, MESFUN7C:def 12;

      then ( lim ( Im F)) is_integrable_on M by A2, A4, A7, A13, A16, Th47;

      then ( R_EAL ( Im ( lim F))) is_integrable_on M by A1, A6, MESFUN7C: 25;

      then

       A17: ( Im ( lim F)) is_integrable_on M;

      

       A18: for x be Element of X st x in E holds (( Re F) # x) is convergent by A14;

      E = ( dom (( Re F) . 0 )) by A1, MESFUN7C:def 11;

      then ( lim ( Re F)) is_integrable_on M by A2, A4, A7, A13, A18, Th47;

      then ( R_EAL ( Re ( lim F))) is_integrable_on M by A1, A6, MESFUN7C: 25;

      then ( Re ( lim F)) is_integrable_on M;

      hence ( lim F) is_integrable_on M by A17, MESFUN6C:def 2;

    end;

    theorem :: MESFUN9C:52

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

    proof

      assume that

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

       A2: E = ( dom P) and

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

       A4: P is_integrable_on M and

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

      

       A6: E = ( dom (( Re F) . 0 )) by A1, MESFUN7C:def 11;

      

       A7: for n be Nat holds (( Re F) . n) is E -measurable & (( Im F) . n) is E -measurable by A3, Lm2;

      

       A8: for x be Element of X, n be Nat st x in E holds ( |.(( Re F) . n).| . x) <= (P . x) & ( |.(( Im F) . n).| . x) <= (P . x)

      proof

        let x be Element of X, n be Nat;

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

        ( Re ((F # x) . n1)) = (( Re (F # x)) . n1) by COMSEQ_3:def 5;

        then

         A9: |.(( Re (F # x)) . n) qua Complex.| <= |.((F # x) . n).| by COMSEQ_3: 13;

        ( Im ((F # x) . n1)) = (( Im (F # x)) . n1) by COMSEQ_3:def 6;

        then

         A10: |.(( Im (F # x)) . n) qua Complex.| <= |.((F # x) . n).| by COMSEQ_3: 13;

        assume

         A11: x in E;

        then ( |.(F . n).| . x) <= (P . x) by A5;

        then |.((F . n) . x).| <= (P . x) by VALUED_1: 18;

        then

         A12: |.((F # x) . n).| <= (P . x) by MESFUN7C:def 9;

        (( Im F) # x) = ( Im (F # x)) by A1, A11, MESFUN7C: 23;

        then

         A13: |.((( Im F) # x) . n1) qua Complex.| <= (P . x) by A12, A10, XXREAL_0: 2;

        (( Re F) # x) = ( Re (F # x)) by A1, A11, MESFUN7C: 23;

        then |.((( Re F) # x) . n) qua Complex.| <= (P . x) by A12, A9, XXREAL_0: 2;

        then

         A14: |.((( Re F) . n) . x) qua Complex.| <= (P . x) by SEQFUNC:def 10;

         |.((( Im F) . n) . x) qua Complex.| <= (P . x) by A13, SEQFUNC:def 10;

        hence ( |.(( Re F) . n).| . x) <= (P . x) & ( |.(( Im F) . n).| . x) <= (P . x) by A14, VALUED_1: 18;

      end;

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

      then

      consider A be Real_Sequence such that

       A15: for n be Nat holds (A . n) = ( Integral (M,(( Re F) . n))) and

       A16: (for x be Element of X st x in E holds (( Re F) # x) is convergent) implies A is convergent & ( lim A) = ( Integral (M,( lim ( Re F)))) by A2, A4, A6, A7, Th48;

      defpred P[ Element of NAT , set] means $2 = ( Integral (M,(F . $1)));

      

       A17: for n be Element of NAT holds ex y be Element of COMPLEX st P[n, y]

      proof

        let n be Element of NAT ;

        ( Integral (M,(F . n))) is Element of COMPLEX by XCMPLX_0:def 2;

        hence thesis;

      end;

      consider I be sequence of COMPLEX such that

       A18: for n be Element of NAT holds P[n, (I . n)] from FUNCT_2:sch 3( A17);

      reconsider I as Complex_Sequence;

      

       A19: E = ( dom (( Im F) . 0 )) by A1, MESFUN7C:def 12;

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

      then

      consider B be Real_Sequence such that

       A20: for n be Nat holds (B . n) = ( Integral (M,(( Im F) . n))) and

       A21: (for x be Element of X st x in E holds (( Im F) # x) is convergent) implies B is convergent & ( lim B) = ( Integral (M,( lim ( Im F)))) by A2, A4, A19, A7, Th48;

      

       A22: for n be Nat holds (( Re F) . n) is_integrable_on M & (( Im F) . n) is_integrable_on M

      proof

        let n be Nat;

         A23:

        now

          let x be Element of X;

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

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

          then ( |.(( Re F) . n).| . x) <= (P . x) by A8;

          hence |.((( Re F) . n) . x) qua Complex.| <= (P . x) by VALUED_1: 18;

        end;

         A24:

        now

          let x be Element of X;

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

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

          then ( |.(( Im F) . n).| . x) <= (P . x) by A8;

          hence |.((( Im F) . n) . x) qua Complex.| <= (P . x) by VALUED_1: 18;

        end;

        

         A25: (( Re F) . n) is E -measurable & (( Im F) . n) is E -measurable by A3, Lm2;

        ( dom (( Re F) . n)) = E & ( dom (( Im F) . n)) = E by A6, A19, MESFUNC8:def 2;

        hence (( Re F) . n) is_integrable_on M & (( Im F) . n) is_integrable_on M by A2, A4, A23, A24, A25, MESFUNC6: 96;

      end;

       A26:

      now

        let n1 be set;

        assume n1 in NAT ;

        then

        reconsider n = n1 as Element of NAT ;

        

         A27: (( Re I) . n) = ( Re (I . n)) & (( Im I) . n) = ( Im (I . n)) by COMSEQ_3:def 5, COMSEQ_3:def 6;

        

         A28: (( Im F) . n) = ( Im (F . n)) by MESFUN7C: 24;

        then

         A29: ( Im (F . n)) is_integrable_on M by A22;

        

         A30: (( Re F) . n) = ( Re (F . n)) by MESFUN7C: 24;

        then ( Re (F . n)) is_integrable_on M by A22;

        then (F . n) is_integrable_on M by A29, MESFUN6C:def 2;

        then

        consider RF,IF be Real such that

         A31: RF = ( Integral (M,( Re (F . n)))) & IF = ( Integral (M,( Im (F . n)))) and

         A32: ( Integral (M,(F . n))) = (RF + (IF * <i> )) by MESFUN6C:def 3;

        (I . n1) = ( Integral (M,(F . n))) by A18;

        then ( Re (I . n1)) = RF & ( Im (I . n1)) = IF by A32, COMPLEX1: 12;

        hence (( Re I) . n1) = (A . n1) & (( Im I) . n1) = (B . n1) by A15, A20, A30, A28, A31, A27;

      end;

      then for x be object st x in NAT holds (( Re I) . x) = (A . x);

      then

       A33: ( Re I) = A;

      take I;

      hereby

        let n be Nat;

        n is Element of NAT by ORDINAL1:def 12;

        hence (I . n) = ( Integral (M,(F . n))) by A18;

      end;

      for x be object st x in NAT holds (( Im I) . x) = (B . x) by A26;

      then

       A34: ( Im I) = B;

      hereby

        assume

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

        then

         A36: ( Integral (M,( lim ( Im F)))) = ( Integral (M,( Im ( lim F)))) by A1, MESFUN7C: 25;

        

         A37: ( lim F) is_integrable_on M & ( Integral (M,( lim ( Re F)))) = ( Integral (M,( Re ( lim F)))) by A1, A2, A3, A4, A5, A35, Th51, MESFUN7C: 25;

         A38:

        now

          let x be Element of X such that

           A39: x in E;

          (F # x) is convergent Complex_Sequence by A35, A39;

          then ( Re (F # x)) is convergent & ( Im (F # x)) is convergent;

          hence (( Re F) # x) is convergent & (( Im F) # x) is convergent by A1, A39, MESFUN7C: 23;

        end;

        hence I is convergent by A16, A21, A33, A34, COMSEQ_3: 42;

        for n be Nat holds (( Re I) . n) = ( Re (I . n)) & (( Im I) . n) = ( Im (I . n)) by COMSEQ_3:def 5, COMSEQ_3:def 6;

        then ( lim I) = (( lim ( Re I)) + (( lim ( Im I)) * <i> )) by A16, A21, A33, A34, A38, COMSEQ_3: 39;

        hence ( lim I) = ( Integral (M,( lim F))) by A16, A21, A33, A34, A38, A37, A36, MESFUN6C:def 3;

      end;

    end;

    definition

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

      :: MESFUN9C:def6

      attr F is uniformly_bounded means ex K be Real st for n be Nat, x be Element of X st x in ( dom (F . 0 )) holds |.((F . n) . x).| <= K;

    end

    theorem :: MESFUN9C:53

    (M . E) < +infty & E = ( dom (F . 0 )) & (for n be Nat holds (F . n) is E -measurable) & F is uniformly_bounded & (for x be Element of X st x in E holds (F # x) is convergent) implies (for n be Nat holds (F . n) is_integrable_on M) & ( lim F) is_integrable_on M & ex I be Complex_Sequence st (for n be Nat holds (I . n) = ( Integral (M,(F . n)))) & I is convergent & ( lim I) = ( Integral (M,( lim F)))

    proof

      assume that

       A1: (M . E) < +infty and

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

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

       A4: F is uniformly_bounded and

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

      consider K be Real such that

       A6: for n be Nat, x be Element of X st x in ( dom (F . 0 )) holds |.((F . n) . x).| <= K by A4;

      

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

      proof

        let x be Element of X;

        assume

         A8: x in E;

        then (F # x) is convergent Complex_Sequence by A5;

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

        hence (( Re F) # x) is convergent by A2, A8, MESFUN7C: 23;

      end;

      for n be Nat, x be Element of X st x in ( dom (( Im F) . 0 )) holds |.((( Im F) . n) . x) qua Complex.| <= K

      proof

        let n be Nat, x be Element of X;

        assume x in ( dom (( Im F) . 0 ));

        then

         A9: x in E by A2, MESFUN7C:def 12;

        then |.((F . n) . x).| <= K by A2, A6;

        then

         A10: |.((F # x) . n).| <= K by MESFUN7C:def 9;

        ( Im ((F # x) . n)) = (( Im (F # x)) . n) by COMSEQ_3:def 6;

        then ( Im ((F # x) . n)) = ((( Im F) # x) . n) by A2, A9, MESFUN7C: 23;

        then |.((( Im F) # x) . n) qua Complex.| <= |.((F # x) . n).| by COMSEQ_3: 13;

        then |.((( Im F) # x) . n) qua Complex.| <= K by A10, XXREAL_0: 2;

        hence thesis by SEQFUNC:def 10;

      end;

      then

       A11: ( Im F) is uniformly_bounded;

      

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

      proof

        let x be Element of X;

        assume

         A13: x in E;

        then (F # x) is convergent Complex_Sequence by A5;

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

        hence (( Im F) # x) is convergent by A2, A13, MESFUN7C: 23;

      end;

      defpred P[ Element of NAT , set] means $2 = ( Integral (M,(F . $1)));

      

       A14: for n be Element of NAT holds ex y be Element of COMPLEX st P[n, y]

      proof

        let n be Element of NAT ;

        take ( Integral (M,(F . n)));

        thus thesis by XCMPLX_0:def 2, TARSKI: 1;

      end;

      consider I be sequence of COMPLEX such that

       A15: for n be Element of NAT holds P[n, (I . n)] from FUNCT_2:sch 3( A14);

      reconsider I as Complex_Sequence;

      

       A16: for n be Nat holds (( Re F) . n) is E -measurable & (( Im F) . n) is E -measurable by A3, Lm2;

      for n be Nat, x be Element of X st x in ( dom (( Re F) . 0 )) holds |.((( Re F) . n) . x) qua Complex.| <= K

      proof

        let n be Nat, x be Element of X;

        assume x in ( dom (( Re F) . 0 ));

        then

         A17: x in E by A2, MESFUN7C:def 11;

        then |.((F . n) . x).| <= K by A2, A6;

        then

         A18: |.((F # x) . n).| <= K by MESFUN7C:def 9;

        ( Re ((F # x) . n)) = (( Re (F # x)) . n) by COMSEQ_3:def 5;

        then ( Re ((F # x) . n)) = ((( Re F) # x) . n) by A2, A17, MESFUN7C: 23;

        then |.((( Re F) # x) . n) qua Complex.| <= |.((F # x) . n).| by COMSEQ_3: 13;

        then |.((( Re F) # x) . n) qua Complex.| <= K by A18, XXREAL_0: 2;

        hence |.((( Re F) . n) . x) qua Complex.| <= K by SEQFUNC:def 10;

      end;

      then

       A19: ( Re F) is uniformly_bounded;

      

       A20: E = ( dom (( Im F) . 0 )) by A2, MESFUN7C:def 12;

      then

      consider B be ExtREAL_sequence such that

       A21: for n be Nat holds (B . n) = ( Integral (M,(( Im F) . n))) and

       A22: B is convergent and

       A23: ( lim B) = ( Integral (M,( lim ( Im F)))) by A1, A16, A12, A11, Th49;

      

       A24: ( lim ( Im F)) is_integrable_on M by A1, A20, A16, A12, A11, Th49;

      then ( R_EAL ( Im ( lim F))) is_integrable_on M by A2, A5, MESFUN7C: 25;

      then

       A25: ( Im ( lim F)) is_integrable_on M;

      

       A26: E = ( dom (( Re F) . 0 )) by A2, MESFUN7C:def 11;

      then

      consider A be ExtREAL_sequence such that

       A27: for n be Nat holds (A . n) = ( Integral (M,(( Re F) . n))) and

       A28: A is convergent and

       A29: ( lim A) = ( Integral (M,( lim ( Re F)))) by A1, A16, A7, A19, Th49;

      thus

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

      proof

        let n be Nat;

        (( Im F) . n) = ( Im (F . n)) by MESFUN7C: 24;

        then

         A31: ( Im (F . n)) is_integrable_on M by A1, A20, A16, A12, A11, Th49;

        (( Re F) . n) = ( Re (F . n)) by MESFUN7C: 24;

        then ( Re (F . n)) is_integrable_on M by A1, A26, A16, A7, A19, Th49;

        hence (F . n) is_integrable_on M by A31, MESFUN6C:def 2;

      end;

      

       A32: for n1 be set st n1 in NAT holds (( R_EAL ( Re I)) . n1) = (A . n1) & (( R_EAL ( Im I)) . n1) = (B . n1)

      proof

        let n1 be set;

        assume n1 in NAT ;

        then

        reconsider n = n1 as Element of NAT ;

        

         A33: (I . n1) = ( Integral (M,(F . n))) by A15;

        (F . n) is_integrable_on M by A30;

        then

        consider RF,IF be Real such that

         A34: RF = ( Integral (M,( Re (F . n)))) and

         A35: IF = ( Integral (M,( Im (F . n)))) and

         A36: ( Integral (M,(F . n))) = (RF + (IF * <i> )) by MESFUN6C:def 3;

        (( Re I) . n) = ( Re (I . n)) by COMSEQ_3:def 5;

        then (( Re F) . n) = ( Re (F . n)) & (( Re I) . n1) = RF by A36, A33, COMPLEX1: 12, MESFUN7C: 24;

        hence (( R_EAL ( Re I)) . n1) = (A . n1) by A27, A34;

        (( Im I) . n) = ( Im (I . n)) by COMSEQ_3:def 6;

        then (( Im F) . n) = ( Im (F . n)) & (( Im I) . n1) = IF by A36, A33, COMPLEX1: 12, MESFUN7C: 24;

        hence (( R_EAL ( Im I)) . n1) = (B . n1) by A21, A35;

      end;

      then for n1 be object st n1 in NAT holds (( R_EAL ( Im I)) . n1) = (B . n1);

      then

       A37: ( Im I) = B;

      

       A38: -infty < ( Integral (M,( lim ( Im F)))) & ( Integral (M,( lim ( Im F)))) < +infty by A24, MESFUNC5: 96;

      

       A39: B is convergent implies B is convergent_to_finite_number by A23, A38, MESFUNC5:def 12;

      then

       A40: ( lim ( Im I)) = ( Integral (M,( lim ( Im F)))) by A22, A23, A37, RINFSUP2: 15;

      

       A41: ( Im I) is convergent by A22, A37, A39, RINFSUP2: 15;

      

       A42: ( lim ( Re F)) is_integrable_on M by A1, A26, A16, A7, A19, Th49;

      then ( R_EAL ( Re ( lim F))) is_integrable_on M by A2, A5, MESFUN7C: 25;

      then ( Re ( lim F)) is_integrable_on M;

      hence

       A43: ( lim F) is_integrable_on M by A25, MESFUN6C:def 2;

      take I;

      for n1 be object st n1 in NAT holds (( R_EAL ( Re I)) . n1) = (A . n1) by A32;

      then

       A44: ( Re I) = A;

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

      proof

        let n be Nat;

        

         A45: (( Re I) . n) = ( Re (I . n)) & (( Im I) . n) = ( Im (I . n)) by COMSEQ_3:def 5, COMSEQ_3:def 6;

        (( Re F) . n) = ( Re (F . n)) by MESFUN7C: 24;

        then

         A46: (( Re I) . n) = ( Integral (M,( Re (F . n)))) by A27, A44;

        (( Im F) . n) = ( Im (F . n)) by MESFUN7C: 24;

        then

         A47: (( Im I) . n) = ( Integral (M,( Im (F . n)))) by A21, A37;

        (I . n) = (( Re (I . n)) + (( Im (I . n)) * <i> )) & (F . n) is_integrable_on M by A30, COMPLEX1: 13;

        hence (I . n) = ( Integral (M,(F . n))) by A45, A46, A47, MESFUN6C:def 3;

      end;

      

       A48: -infty < ( Integral (M,( lim ( Re F)))) & ( Integral (M,( lim ( Re F)))) < +infty by A42, MESFUNC5: 96;

      

       A49: A is convergent implies A is convergent_to_finite_number by A29, A48, MESFUNC5:def 12;

      then

       A50: ( Re I) is convergent by A28, A44, RINFSUP2: 15;

      hence I is convergent by A41, COMSEQ_3: 42;

      for n be Nat holds (( Re I) . n) = ( Re (I . n)) & (( Im I) . n) = ( Im (I . n)) by COMSEQ_3:def 5, COMSEQ_3:def 6;

      then

       A51: ( lim I) = (( lim ( Re I)) + (( lim ( Im I)) * <i> )) by A50, A41, COMSEQ_3: 39;

      

       A52: ( Integral (M,( lim ( Re F)))) = ( Integral (M,( Re ( lim F)))) & ( Integral (M,( lim ( Im F)))) = ( Integral (M,( Im ( lim F)))) by A2, A5, MESFUN7C: 25;

      ( lim ( Re I)) = ( Integral (M,( lim ( Re F)))) by A28, A29, A44, A49, RINFSUP2: 15;

      hence ( lim I) = ( Integral (M,( lim F))) by A43, A40, A51, A52, MESFUN6C:def 3;

    end;

    definition

      let X be set, F be Functional_Sequence of X, COMPLEX , f be PartFunc of X, COMPLEX ;

      :: MESFUN9C:def7

      pred F is_uniformly_convergent_to f means F is with_the_same_dom & ( dom (F . 0 )) = ( dom f) & for e be Real st e > 0 holds ex N be Nat st for n be Nat, x be Element of X st n >= N & x in ( dom (F . 0 )) holds |.(((F . n) . x) - (f . x)).| < e;

    end

    theorem :: MESFUN9C:54

    (M . E) < +infty & E = ( dom (F . 0 )) & (for n be Nat holds (F . n) is_integrable_on M) & F is_uniformly_convergent_to f implies f is_integrable_on M & ex I be Complex_Sequence st (for n be Nat holds (I . n) = ( Integral (M,(F . n)))) & I is convergent & ( lim I) = ( Integral (M,f))

    proof

      assume that

       A1: (M . E) < +infty and

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

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

       A4: F is_uniformly_convergent_to f;

      

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

      proof

        let n be Nat;

        (F . n) is_integrable_on M by A3;

        then ( Im (F . n)) is_integrable_on M by MESFUN6C:def 2;

        hence (( Im F) . n) is_integrable_on M by MESFUN7C: 24;

      end;

      

       A6: ( dom (F . 0 )) = ( dom f) by A4;

      

       A7: for e be Real st e > 0 holds ex N be Nat st for n be Nat, x be Element of X st n >= N & x in ( dom (( Im F) . 0 )) holds |.(((( Im F) . n) . x) - (( Im f) . x)) qua Complex.| < e

      proof

        let e be Real;

        assume e > 0 ;

        then

        consider N be Nat such that

         A8: for n be Nat, x be Element of X st n >= N & x in ( dom (F . 0 )) holds |.(((F . n) . x) - (f . x)).| < e by A4;

        for n be Nat, x be Element of X st n >= N & x in ( dom (( Im F) . 0 )) holds |.(((( Im F) . n) . x) - (( Im f) . x)) qua Complex.| < e

        proof

          let n be Nat, x be Element of X;

          assume that

           A9: n >= N and

           A10: x in ( dom (( Im F) . 0 ));

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

          

           A11: x in ( dom (F . 0 )) by A10, MESFUN7C:def 12;

          then |.(((F . n) . x) - (f . x)).| < e by A8, A9;

          then

           A12: |.(((F # x) . n) - (f . x)).| < e by MESFUN7C:def 9;

          

           A13: ( Im (((F # x) . n) - (f . x))) = (( Im ((F # x) . n)) - ( Im (f . x))) by COMPLEX1: 19;

          

           A14: |.(( Im ((F # x) . n)) - ( Im (f . x))) qua Complex.| <= |.(((F # x) . n) - (f . x)).| by A13, COMSEQ_3: 13;

          x in ( dom ( Im f)) by A6, A11, COMSEQ_3:def 4;

          then

           A15: ( Im (f . x)) = (( Im f) . x) by COMSEQ_3:def 4;

          ( Im ((F # x) . n1)) = (( Im (F # x)) . n) by COMSEQ_3:def 6

          .= ((( Im F) # x) . n1) by A11, MESFUN7C: 23

          .= ((( Im F) . n) . x) by SEQFUNC:def 10;

          hence |.(((( Im F) . n) . x) - (( Im f) . x)) qua Complex.| < e by A12, A14, A15, XXREAL_0: 2;

        end;

        hence thesis;

      end;

      ( dom (( Im F) . 0 )) = ( dom f) by A6, MESFUN7C:def 12;

      then ( dom (( Im F) . 0 )) = ( dom ( Im f)) by COMSEQ_3:def 4;

      then

       A16: ( Im F) is_uniformly_convergent_to ( Im f) by A7;

      

       A17: for e be Real st e > 0 holds ex N be Nat st for n be Nat, x be Element of X st n >= N & x in ( dom (( Re F) . 0 )) holds |.(((( Re F) . n) . x) - (( Re f) . x)) qua Complex.| < e

      proof

        let e be Real;

        assume e > 0 ;

        then

        consider N be Nat such that

         A18: for n be Nat, x be Element of X st n >= N & x in ( dom (F . 0 )) holds |.(((F . n) . x) - (f . x)).| < e by A4;

        for n be Nat, x be Element of X st n >= N & x in ( dom (( Re F) . 0 )) holds |.(((( Re F) . n) . x) - (( Re f) . x)) qua Complex.| < e

        proof

          let n be Nat, x be Element of X;

          assume that

           A19: n >= N and

           A20: x in ( dom (( Re F) . 0 ));

          

           A21: x in ( dom (F . 0 )) by A20, MESFUN7C:def 11;

          

           A22: ( Re (((F # x) . n) - (f . x))) = (( Re ((F # x) . n)) - ( Re (f . x))) by COMPLEX1: 19;

          ((F . n) . x) = ((F # x) . n) by MESFUN7C:def 9;

          then

           A23: |.(((F # x) . n) - (f . x)).| < e by A18, A19, A21;

          x in ( dom ( Re f)) by A6, A21, COMSEQ_3:def 3;

          then

           A24: ( Re (f . x)) = (( Re f) . x) by COMSEQ_3:def 3;

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

          

           A25: |.(( Re ((F # x) . n)) - ( Re (f . x))) qua Complex.| <= |.(((F # x) . n) - (f . x)).| by A22, COMSEQ_3: 13;

          ( Re ((F # x) . n)) = (( Re (F # x)) . n1) by COMSEQ_3:def 5

          .= ((( Re F) # x) . n) by A21, MESFUN7C: 23

          .= ((( Re F) . n1) . x) by SEQFUNC:def 10;

          hence |.(((( Re F) . n) . x) - (( Re f) . x)) qua Complex.| < e by A23, A25, A24, XXREAL_0: 2;

        end;

        hence thesis;

      end;

      ( dom (( Re F) . 0 )) = ( dom f) by A6, MESFUN7C:def 11;

      then ( dom (( Re F) . 0 )) = ( dom ( Re f)) by COMSEQ_3:def 3;

      then

       A26: ( Re F) is_uniformly_convergent_to ( Re f) by A17;

      defpred P[ Element of NAT , set] means $2 = ( Integral (M,(F . $1)));

      

       A27: for n be Element of NAT holds ex y be Element of COMPLEX st P[n, y]

      proof

        let n be Element of NAT ;

        ( Integral (M,(F . n))) is Element of COMPLEX by XCMPLX_0:def 2;

        hence thesis;

      end;

      consider I be sequence of COMPLEX such that

       A28: for n be Element of NAT holds P[n, (I . n)] from FUNCT_2:sch 3( A27);

      

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

      proof

        let n be Nat;

        (F . n) is_integrable_on M by A3;

        then ( Re (F . n)) is_integrable_on M by MESFUN6C:def 2;

        hence (( Re F) . n) is_integrable_on M by MESFUN7C: 24;

      end;

      

       A30: E = ( dom (( Im F) . 0 )) by A2, MESFUN7C:def 12;

      then

       A31: ( Im f) is_integrable_on M by A1, A5, A16, Th50;

      

       A32: E = ( dom (( Re F) . 0 )) by A2, MESFUN7C:def 11;

      then

      consider A be ExtREAL_sequence such that

       A33: for n be Nat holds (A . n) = ( Integral (M,(( Re F) . n))) and

       A34: A is convergent and

       A35: ( lim A) = ( Integral (M,( Re f))) by A1, A29, A26, Th50;

      

       A36: ( Re f) is_integrable_on M by A1, A32, A29, A26, Th50;

      hence

       A37: f is_integrable_on M by A31, MESFUN6C:def 2;

      reconsider I as Complex_Sequence;

      consider B be ExtREAL_sequence such that

       A38: for n be Nat holds (B . n) = ( Integral (M,(( Im F) . n))) and

       A39: B is convergent and

       A40: ( lim B) = ( Integral (M,( Im f))) by A1, A30, A5, A16, Th50;

       A41:

      now

        let n1 be set;

        assume n1 in NAT ;

        then

        reconsider n = n1 as Element of NAT ;

        

         A42: (( Re F) . n) = ( Re (F . n)) & (( Im F) . n) = ( Im (F . n)) by MESFUN7C: 24;

        (F . n) is_integrable_on M by A3;

        then

        consider RF,IF be Real such that

         A43: RF = ( Integral (M,( Re (F . n)))) & IF = ( Integral (M,( Im (F . n)))) and

         A44: ( Integral (M,(F . n))) = (RF + (IF * <i> )) by MESFUN6C:def 3;

        

         A45: (( Re I) . n) = ( Re (I . n)) & (( Im I) . n) = ( Im (I . n)) by COMSEQ_3:def 5, COMSEQ_3:def 6;

        (I . n1) = ( Integral (M,(F . n))) by A28;

        then ( Re (I . n1)) = RF & ( Im (I . n1)) = IF by A44, COMPLEX1: 12;

        hence (( R_EAL ( Re I)) . n1) = (A . n1) & (( R_EAL ( Im I)) . n1) = (B . n1) by A33, A38, A42, A45, A43;

      end;

      then for x be object st x in NAT holds (( R_EAL ( Im I)) . x) = (B . x);

      then

       A46: ( Im I) = B;

      

       A47: -infty < ( Integral (M,( Im f))) & ( Integral (M,( Im f))) < +infty by A31, MESFUNC6: 90;

      

       A48: B is convergent implies B is convergent_to_finite_number by A40, A47, MESFUNC5:def 12;

      then

       A49: ( lim ( Im I)) = ( Integral (M,( Im f))) by A39, A40, A46, RINFSUP2: 15;

      

       A50: ( Im I) is convergent by A39, A46, A48, RINFSUP2: 15;

      take I;

      for x be object st x in NAT holds (( R_EAL ( Re I)) . x) = (A . x) by A41;

      then

       A51: ( Re I) = A;

      thus 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;

        (( Re I) . n1) = ( Re (I . n1)) & (( Im I) . n1) = ( Im (I . n1)) by COMSEQ_3:def 5, COMSEQ_3:def 6;

        then

         A52: (I . n) = ((( Re I) . n) + ((( Im I) . n) * <i> )) by COMPLEX1: 13;

        (( Re F) . n) = ( Re (F . n)) by MESFUN7C: 24;

        then

         A53: (( Re I) . n) = ( Integral (M,( Re (F . n)))) by A33, A51;

        (( Im F) . n) = ( Im (F . n)) by MESFUN7C: 24;

        then

         A54: (( Im I) . n) = ( Integral (M,( Im (F . n)))) by A38, A46;

        (F . n) is_integrable_on M by A3;

        hence (I . n) = ( Integral (M,(F . n))) by A52, A53, A54, MESFUN6C:def 3;

      end;

      

       A55: -infty < ( Integral (M,( Re f))) & ( Integral (M,( Re f))) < +infty by A36, MESFUNC6: 90;

      

       A56: A is convergent implies A is convergent_to_finite_number by A35, A55, MESFUNC5:def 12;

      then

       A57: ( Re I) is convergent by A34, A51, RINFSUP2: 15;

      hence I is convergent by A50, COMSEQ_3: 42;

      for n be Nat holds (( Re I) . n) = ( Re (I . n)) & (( Im I) . n) = ( Im (I . n)) by COMSEQ_3:def 5, COMSEQ_3:def 6;

      then

       A58: ( lim I) = (( lim ( Re I)) + (( lim ( Im I)) * <i> )) by A57, A50, COMSEQ_3: 39;

      ( lim ( Re I)) = ( Integral (M,( Re f))) by A34, A35, A51, A56, RINFSUP2: 15;

      hence ( lim I) = ( Integral (M,f)) by A37, A49, A58, MESFUN6C:def 3;

    end;