:: MESFUN9C semantic presentation

begin


definition
let X, Y be set ;
let F be Functional_Sequence of X,Y;
let D be set ;
funcF || D ->  Functional_Sequence of X,Y means :Def1: :: MESFUN9C:def 1
 for n being Nat holds it . n = (F . n) | D;
existence
 ex b1 being Functional_Sequence of X,Y st
for n being Nat holds b1 . n = (F . n) | D
proof
deffunc H1( Nat) ->  Element of K6(K7(X,Y)) = (F . $1) | D;
 ex G being Functional_Sequence of X,Y st
for n being Nat holds G . n = H1(n) from SEQFUNC:sch_1();
hence  ex b1 being Functional_Sequence of X,Y st
for n being Nat holds b1 . n = (F . n) | D ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Functional_Sequence of X,Y st ( for n being Nat holds b1 . n = (F . n) | D ) & ( for n being Nat holds b2 . n = (F . n) | D ) holds
b1 = b2
proof
let A, B be Functional_Sequence of X,Y; ::_thesis: ( ( for n being Nat holds A . n = (F . n) | D ) & ( for n being Nat holds B . n = (F . n) | D ) implies A = B )
assume that
A1: for n being Nat holds A . n = (F . n) | D and
A2: for n being Nat holds B . n = (F . n) | D ; ::_thesis: A = B
let x be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: A . x = B . x
thus A . x = (F . x) | D by A1
.= B . x by A2 ; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines || MESFUN9C:def_1_:_
 for X, Y being set
for F being Functional_Sequence of X,Y
for D being set
for b5 being Functional_Sequence of X,Y holds
( b5 = F || D iff for n being Nat holds b5 . n = (F . n) | D );

theorem Th1: :: MESFUN9C:1
for X being non empty set
for F being Functional_Sequence of X,REAL
for x being Element of X
for D being set st x in D & F # x is convergent holds
(F || D) # x is convergent
proof
let X be non empty set ; ::_thesis: for F being Functional_Sequence of X,REAL
for x being Element of X
for D being set st x in D & F # x is convergent holds
(F || D) # x is convergent
let F be Functional_Sequence of X,REAL; ::_thesis: for x being Element of X
for D being set st x in D & F # x is convergent holds
(F || D) # x is convergent
let x be Element of X; ::_thesis: for D being set st x in D & F # x is convergent holds
(F || D) # x is convergent
let D be set ; ::_thesis: ( x in D & F # x is convergent implies (F || D) # x is convergent )
set G = F || D;
assume A1: x in D ; ::_thesis: ( not F # x is convergent or (F || D) # x is convergent )
A2: (R_EAL (F || D)) # x = (F || D) # x by MESFUN7C:1;
assume  F # x is convergent ; ::_thesis: (F || D) # 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 being Nat holds (R_EAL (F || D)) . n = ((R_EAL F) . n) | D by Def1;
then  (R_EAL (F || D)) # x is convergent_to_finite_number by A1, A3, MESFUNC9:12;
hence  (F || D) # x is convergent by A2, RINFSUP2:15; ::_thesis: verum
end;

theorem Th2: :: MESFUN9C:2
for X, Y, D being set
for F being 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 ; ::_thesis: for F being Functional_Sequence of X,Y st F is with_the_same_dom holds
F || D is with_the_same_dom
let F be Functional_Sequence of X,Y; ::_thesis: ( F is with_the_same_dom implies F || D is with_the_same_dom )
assume A1: F is with_the_same_dom ; ::_thesis: F || D is with_the_same_dom
let n, m be Nat; :: according to MESFUNC8:def_2 ::_thesis: dom ((F || D) . n) = dom ((F || D) . m)
set G = F || D;
 (F || D) . m = (F . m) | D by Def1;
then A2: dom ((F || D) . m) = (dom (F . m)) /\ D by RELAT_1:61;
 (F || D) . n = (F . n) | D by Def1;
then  dom ((F || D) . n) = (dom (F . n)) /\ D by RELAT_1:61;
hence  dom ((F || D) . n) = dom ((F || D) . m) by A1, A2, MESFUNC8:def_2; ::_thesis: verum
end;

theorem Th3: :: MESFUN9C:3
for X being non empty set
for F being Functional_Sequence of X,REAL
for D being set st D c= dom (F . 0) & ( for x being Element of X st x in D holds
F # x is convergent ) holds
(lim F) | D = lim (F || D)
proof
let X be non empty set ; ::_thesis: for F being Functional_Sequence of X,REAL
for D being set st D c= dom (F . 0) & ( for x being Element of X st x in D holds
F # x is convergent ) holds
(lim F) | D = lim (F || D)
let F be Functional_Sequence of X,REAL; ::_thesis: for D being set st D c= dom (F . 0) & ( for x being Element of X st x in D holds
F # x is convergent ) holds
(lim F) | D = lim (F || D)
let D be set ; ::_thesis: ( D c= dom (F . 0) & ( for x being Element of X st x in D holds
F # x is convergent ) implies (lim F) | D = lim (F || D) )
set G = F || D;
assume that
A1: D c= dom (F . 0) and
A2: for x being Element of X st x in D holds
F # x is convergent ; ::_thesis: (lim F) | D = lim (F || D)
A3: for x being Element of X st x in D holds
(R_EAL F) # x is convergent
proof
let x be Element of X; ::_thesis: ( x in D implies (R_EAL F) # x is convergent )
assume  x in D ; ::_thesis: (R_EAL F) # x is convergent
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; ::_thesis: verum
end;
 for n being Nat holds (R_EAL (F || D)) . n = ((R_EAL F) . n) | D by Def1;
hence  (lim F) | D = lim (F || D) by A1, A3, MESFUNC9:19; ::_thesis: verum
end;

theorem Th4: :: MESFUN9C:4
for X being non empty set
for S being SigmaField of X
for E being Element of S
for F being Functional_Sequence of X,REAL
for n being Nat st F is with_the_same_dom & E c= dom (F . 0) & ( for m being Nat holds F . m is_measurable_on E ) holds
(F || E) . n is_measurable_on E
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for E being Element of S
for F being Functional_Sequence of X,REAL
for n being Nat st F is with_the_same_dom & E c= dom (F . 0) & ( for m being Nat holds F . m is_measurable_on E ) holds
(F || E) . n is_measurable_on E
let S be SigmaField of X; ::_thesis: for E being Element of S
for F being Functional_Sequence of X,REAL
for n being Nat st F is with_the_same_dom & E c= dom (F . 0) & ( for m being Nat holds F . m is_measurable_on E ) holds
(F || E) . n is_measurable_on E
let E be Element of S; ::_thesis: for F being Functional_Sequence of X,REAL
for n being Nat st F is with_the_same_dom & E c= dom (F . 0) & ( for m being Nat holds F . m is_measurable_on E ) holds
(F || E) . n is_measurable_on E
let F be Functional_Sequence of X,REAL; ::_thesis: for n being Nat st F is with_the_same_dom & E c= dom (F . 0) & ( for m being Nat holds F . m is_measurable_on E ) holds
(F || E) . n is_measurable_on E
let n be Nat; ::_thesis: ( F is with_the_same_dom & E c= dom (F . 0) & ( for m being Nat holds F . m is_measurable_on E ) implies (F || E) . n is_measurable_on E )
set G = F || E;
assume A1: ( F is with_the_same_dom & E c= dom (F . 0) ) ; ::_thesis: ( ex m being Nat st not F . m is_measurable_on E or (F || E) . n is_measurable_on E )
assume A2: for m being Nat holds F . m is_measurable_on E ; ::_thesis: (F || E) . n is_measurable_on E
 for m being Nat holds
( (R_EAL F) . m is_measurable_on E & (R_EAL (F || E)) . m = ((R_EAL F) . m) | E )
proof
let m be Nat; ::_thesis: ( (R_EAL F) . m is_measurable_on E & (R_EAL (F || E)) . m = ((R_EAL F) . m) | E )
 F . m is_measurable_on E by A2;
then  R_EAL (F . m) is_measurable_on E by MESFUNC6:def_1;
hence  (R_EAL F) . m is_measurable_on E ; ::_thesis: (R_EAL (F || E)) . m = ((R_EAL F) . m) | E
thus  (R_EAL (F || E)) . m = ((R_EAL F) . m) | E by Def1; ::_thesis: verum
end;
then  R_EAL ((F || E) . n) is_measurable_on E by A1, MESFUNC9:20;
hence  (F || E) . n is_measurable_on E by MESFUNC6:def_1; ::_thesis: verum
end;

theorem Th5: :: MESFUN9C:5
for seq being Real_Sequence holds Partial_Sums (R_EAL seq) = R_EAL (Partial_Sums seq)
proof
let seq be Real_Sequence; ::_thesis: Partial_Sums (R_EAL seq) = R_EAL (Partial_Sums seq)
defpred S1[ Element of NAT ] means (Partial_Sums (R_EAL seq)) . $1 = (R_EAL (Partial_Sums seq)) . $1;
A1: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume  S1[k] ; ::_thesis: S1[k + 1]
then (Partial_Sums (R_EAL seq)) . (k + 1) = (R_EAL ((Partial_Sums seq) . k)) + (R_EAL (seq . (k + 1))) by MESFUNC9:def_1
.= R_EAL (((Partial_Sums seq) . k) + (seq . (k + 1))) by MESFUN6C:1 ;
hence  S1[k + 1] by SERIES_1:def_1; ::_thesis: verum
end;
 (Partial_Sums (R_EAL seq)) . 0 = R_EAL (seq . 0) by MESFUNC9:def_1;
then A2: S1[ 0 ] by SERIES_1:def_1;
 for i being Element of NAT holds S1[i] from NAT_1:sch_1(A2, A1);
hence  Partial_Sums (R_EAL seq) = R_EAL (Partial_Sums seq) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th6: :: MESFUN9C:6
for X being non empty set
for S being SigmaField of X
for E being Element of S
for F being Functional_Sequence of X,REAL st ( for x being Element of X st x in E holds
F # x is summable ) holds
for x being Element of X st x in E holds
(F || E) # x is summable
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for E being Element of S
for F being Functional_Sequence of X,REAL st ( for x being Element of X st x in E holds
F # x is summable ) holds
for x being Element of X st x in E holds
(F || E) # x is summable
let S be SigmaField of X; ::_thesis: for E being Element of S
for F being Functional_Sequence of X,REAL st ( for x being Element of X st x in E holds
F # x is summable ) holds
for x being Element of X st x in E holds
(F || E) # x is summable
let E be Element of S; ::_thesis: for F being Functional_Sequence of X,REAL st ( for x being Element of X st x in E holds
F # x is summable ) holds
for x being Element of X st x in E holds
(F || E) # x is summable
let F be Functional_Sequence of X,REAL; ::_thesis: ( ( for x being Element of X st x in E holds
F # x is summable ) implies for x being Element of X st x in E holds
(F || E) # x is summable )
set G = F || E;
assume A1: for x being Element of X st x in E holds
F # x is summable ; ::_thesis: for x being Element of X st x in E holds
(F || E) # x is summable
let x be Element of X; ::_thesis: ( x in E implies (F || E) # x is summable )
assume A2: x in E ; ::_thesis: (F || E) # x is summable
 for n being Element of NAT holds (F # x) . n = ((F || E) # x) . n
proof
let n be Element of NAT ; ::_thesis: (F # x) . n = ((F || E) # x) . n
 (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 = ((F || E) . n) . x by Def1;
hence  (F # x) . n = ((F || E) # x) . n by SEQFUNC:def_10; ::_thesis: verum
end;
then A3: Partial_Sums (F # x) = Partial_Sums ((F || E) # x) by FUNCT_2:63;
 F # x is summable by A1, A2;
then  Partial_Sums (F # x) is convergent by SERIES_1:def_2;
hence  (F || E) # x is summable by A3, SERIES_1:def_2; ::_thesis: verum
end;

definition
let X be non empty set ;
let F be Functional_Sequence of X,REAL;
func Partial_Sums F ->  Functional_Sequence of X,REAL means :Def2: :: MESFUN9C:def 2
( it . 0 = F . 0 & ( for n being Nat holds it . (n + 1) = (it . n) + (F . (n + 1)) ) );
existence
 ex b1 being Functional_Sequence of X,REAL st
( b1 . 0 = F . 0 & ( for n being Nat holds b1 . (n + 1) = (b1 . n) + (F . (n + 1)) ) )
proof
defpred S1[ Element of NAT , set , set ] means ( ( $2 is not PartFunc of X,REAL & $3 = F . $1 ) or ( $2 is PartFunc of X,REAL & ( for F2 being PartFunc of X,REAL st F2 = $2 holds
$3 = F2 + (F . ($1 + 1)) ) ) );
A1: for n being Element of NAT
for x being set ex y being set st S1[n,x,y]
proof
let n be Element of NAT ; ::_thesis: for x being set ex y being set st S1[n,x,y]
let x be set ; ::_thesis: ex y being set st S1[n,x,y]
now__::_thesis:_(_x_is_PartFunc_of_X,REAL_implies_ex_y_being_Element_of_K6(K7(X,REAL))_st_
(_(_x_is_not_PartFunc_of_X,REAL_&_y_=_F_._n_)_or_(_x_is_PartFunc_of_X,REAL_&_(_for_F2_being_PartFunc_of_X,REAL_st_F2_=_x_holds_
y_=_F2_+_(F_._(n_+_1))_)_)_)_)
assume  x is PartFunc of X,REAL ; ::_thesis: ex y being Element of K6(K7(X,REAL)) st
( ( x is not PartFunc of X,REAL & y = F . n ) or ( x is PartFunc of X,REAL & ( for F2 being PartFunc of X,REAL st F2 = x holds
y = F2 + (F . (n + 1)) ) ) )
then reconsider G2 = x as PartFunc of X,REAL ;
take y = G2 + (F . (n + 1)); ::_thesis: ( ( x is not PartFunc of X,REAL & y = F . n ) or ( x is PartFunc of X,REAL & ( for F2 being PartFunc of X,REAL st F2 = x holds
y = F2 + (F . (n + 1)) ) ) )
thus  ( ( x is not PartFunc of X,REAL & y = F . n ) or ( x is PartFunc of X,REAL & ( for F2 being PartFunc of X,REAL st F2 = x holds
y = F2 + (F . (n + 1)) ) ) ) ; ::_thesis: verum
end;
hence  ex y being set st S1[n,x,y] ; ::_thesis: verum
end;
consider IT being Function such that
A2: ( dom IT = NAT & IT . 0 = F . 0 & ( for n being Element of NAT holds S1[n,IT . n,IT . (n + 1)] ) ) from RECDEF_1:sch_1(A1);
now__::_thesis:_for_f_being_set_st_f_in_rng_IT_holds_
f_in_PFuncs_(X,REAL)
defpred S2[ Element of NAT ] means IT . $1 is PartFunc of X,REAL;
let f be set ; ::_thesis: ( f in rng IT implies f in PFuncs (X,REAL) )
assume  f in rng IT ; ::_thesis: f in PFuncs (X,REAL)
then consider m being set  such that
A3: m in dom IT and
A4: f = IT . m by FUNCT_1:def_3;
reconsider m = m as Element of NAT by A2, A3;
A5: for n being Element of NAT st S2[n] holds
S2[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] )
assume  S2[n] ; ::_thesis: S2[n + 1]
then reconsider F2 = IT . n as PartFunc of X,REAL ;
 IT . (n + 1) = F2 + (F . (n + 1)) by A2;
hence  S2[n + 1] ; ::_thesis: verum
end;
A6: S2[ 0 ] by A2;
 for n being Element of NAT holds S2[n] from NAT_1:sch_1(A6, A5);
then  IT . m is PartFunc of X,REAL ;
hence  f in PFuncs (X,REAL) by A4, PARTFUN1:45; ::_thesis: verum
end;
then  rng IT c= PFuncs (X,REAL) by TARSKI:def_3;
then reconsider IT = IT as Functional_Sequence of X,REAL by A2, FUNCT_2:def_1, RELSET_1:4;
take  IT ; ::_thesis: ( IT . 0 = F . 0 & ( for n being Nat holds IT . (n + 1) = (IT . n) + (F . (n + 1)) ) )
 for n being Nat holds IT . (n + 1) = (IT . n) + (F . (n + 1))
proof
let n be Nat; ::_thesis: IT . (n + 1) = (IT . n) + (F . (n + 1))
 n is Element of NAT by ORDINAL1:def_12;
hence  IT . (n + 1) = (IT . n) + (F . (n + 1)) by A2; ::_thesis: verum
end;
hence  ( IT . 0 = F . 0 & ( for n being Nat holds IT . (n + 1) = (IT . n) + (F . (n + 1)) ) ) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Functional_Sequence of X,REAL st b1 . 0 = F . 0 & ( for n being Nat holds b1 . (n + 1) = (b1 . n) + (F . (n + 1)) ) & b2 . 0 = F . 0 & ( for n being Nat holds b2 . (n + 1) = (b2 . n) + (F . (n + 1)) ) holds
b1 = b2
proof
let PS1, PS2 be Functional_Sequence of X,REAL; ::_thesis: ( PS1 . 0 = F . 0 & ( for n being Nat holds PS1 . (n + 1) = (PS1 . n) + (F . (n + 1)) ) & PS2 . 0 = F . 0 & ( for n being Nat holds PS2 . (n + 1) = (PS2 . n) + (F . (n + 1)) ) implies PS1 = PS2 )
assume that
A7: PS1 . 0 = F . 0 and
A8: for n being Nat holds PS1 . (n + 1) = (PS1 . n) + (F . (n + 1)) and
A9: PS2 . 0 = F . 0 and
A10: for n being Nat holds PS2 . (n + 1) = (PS2 . n) + (F . (n + 1)) ; ::_thesis: PS1 = PS2
defpred S1[ Nat] means PS1 . $1 = PS2 . $1;
A11: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A12: S1[n] ; ::_thesis: S1[n + 1]
 PS1 . (n + 1) = (PS1 . n) + (F . (n + 1)) by A8;
hence  PS1 . (n + 1) = PS2 . (n + 1) by A10, A12; ::_thesis: verum
end;
A13: S1[ 0 ] by A7, A9;
 for n being Nat holds S1[n] from NAT_1:sch_2(A13, A11);
then  for m being Element of NAT holds PS1 . m = PS2 . m ;
hence  PS1 = PS2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines Partial_Sums MESFUN9C:def_2_:_
 for X being non empty set
for F, b3 being Functional_Sequence of X,REAL holds
( b3 = Partial_Sums F iff ( b3 . 0 = F . 0 & ( for n being Nat holds b3 . (n + 1) = (b3 . n) + (F . (n + 1)) ) ) );

theorem Th7: :: MESFUN9C:7
for X being non empty set
for F being Functional_Sequence of X,REAL holds Partial_Sums (R_EAL F) = R_EAL (Partial_Sums F)
proof
let X be non empty set ; ::_thesis: for F being Functional_Sequence of X,REAL holds Partial_Sums (R_EAL F) = R_EAL (Partial_Sums F)
let F be Functional_Sequence of X,REAL; ::_thesis: Partial_Sums (R_EAL F) = R_EAL (Partial_Sums F)
defpred S1[ Element of NAT ] means (Partial_Sums (R_EAL F)) . $1 = (R_EAL (Partial_Sums F)) . $1;
A1: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume  S1[k] ; ::_thesis: S1[k + 1]
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  S1[k + 1] by Def2; ::_thesis: verum
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: S1[ 0 ] ;
 for i being Element of NAT holds S1[i] from NAT_1:sch_1(A2, A1);
hence  Partial_Sums (R_EAL F) = R_EAL (Partial_Sums F) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th8: :: MESFUN9C:8
for X being non empty set
for F being Functional_Sequence of X,REAL
for n, m being Nat
for z being set st z in dom ((Partial_Sums F) . n) & m <= n holds
( z in dom ((Partial_Sums F) . m) & z in dom (F . m) )
proof
let X be non empty set ; ::_thesis: for F being Functional_Sequence of X,REAL
for n, m being Nat
for z being set st z in dom ((Partial_Sums F) . n) & m <= n holds
( z in dom ((Partial_Sums F) . m) & z in dom (F . m) )
let F be Functional_Sequence of X,REAL; ::_thesis: for n, m being Nat
for z being set st z in dom ((Partial_Sums F) . n) & m <= n holds
( z in dom ((Partial_Sums F) . m) & z in dom (F . m) )
let n, m be Nat; ::_thesis: for z being set st z in dom ((Partial_Sums F) . n) & m <= n holds
( z in dom ((Partial_Sums F) . m) & z in dom (F . m) )
let z be set ; ::_thesis: ( z in dom ((Partial_Sums F) . n) & m <= n implies ( z in dom ((Partial_Sums F) . m) & z in dom (F . m) ) )
 (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  ( z in dom ((Partial_Sums F) . n) & m <= n implies ( z in dom ((Partial_Sums F) . m) & z in dom (F . m) ) ) by A1, MESFUNC9:22; ::_thesis: verum
end;

theorem Th9: :: MESFUN9C:9
for X being non empty set
for F being Functional_Sequence of X,REAL holds R_EAL F is additive
proof
let X be non empty set ; ::_thesis: for F being Functional_Sequence of X,REAL holds R_EAL F is additive
let F be Functional_Sequence of X,REAL; ::_thesis: R_EAL F is additive
now__::_thesis:_for_n,_m_being_Nat_st_n_<>_m_holds_
for_x_being_set_holds_
(_not_x_in_(dom_((R_EAL_F)_._n))_/\_(dom_((R_EAL_F)_._m))_or_((R_EAL_F)_._n)_._x_<>_+infty_or_((R_EAL_F)_._m)_._x_<>_-infty_)
let n, m be Nat; ::_thesis: ( n <> m implies for x being set holds
( not x in (dom ((R_EAL F) . n)) /\ (dom ((R_EAL F) . m)) or ((R_EAL F) . n) . x <> +infty or ((R_EAL F) . m) . x <> -infty ) )
assume  n <> m ; ::_thesis: for x being set holds
( not x in (dom ((R_EAL F) . n)) /\ (dom ((R_EAL F) . m)) or ((R_EAL F) . n) . x <> +infty or ((R_EAL F) . m) . x <> -infty )
let x be set ; ::_thesis: ( not x in (dom ((R_EAL F) . n)) /\ (dom ((R_EAL F) . m)) or ((R_EAL F) . n) . x <> +infty or ((R_EAL F) . m) . x <> -infty )
assume  x in (dom ((R_EAL F) . n)) /\ (dom ((R_EAL F) . m)) ; ::_thesis: ( ((R_EAL F) . n) . x <> +infty or ((R_EAL F) . m) . x <> -infty )
 (R_EAL F) . n = R_EAL (F . n) ;
hence  ( ((R_EAL F) . n) . x <> +infty or ((R_EAL F) . m) . x <> -infty ) ; ::_thesis: verum
end;
hence  R_EAL F is additive by MESFUNC9:def_5; ::_thesis: verum
end;

theorem Th10: :: MESFUN9C:10
for X being non empty set
for F being Functional_Sequence of X,REAL
for n being Nat holds dom ((Partial_Sums F) . n) = meet  {  (dom (F . k)) where k is Element of NAT : k <= n  }
proof
let X be non empty set ; ::_thesis: for F being Functional_Sequence of X,REAL
for n being Nat holds dom ((Partial_Sums F) . n) = meet  {  (dom (F . k)) where k is Element of NAT : k <= n  }
let F be Functional_Sequence of X,REAL; ::_thesis: for n being Nat holds dom ((Partial_Sums F) . n) = meet  {  (dom (F . k)) where k is Element of NAT : k <= n  }
let n be Nat; ::_thesis: dom ((Partial_Sums F) . n) = meet  {  (dom (F . k)) where k is Element of NAT : k <= n  }
 ( dom ((Partial_Sums (R_EAL F)) . n) = meet  {  (dom ((R_EAL F) . k)) where k is Element of NAT : k <= n  }  & (Partial_Sums (R_EAL F)) . n = (R_EAL (Partial_Sums F)) . n ) by Th7, Th9, MESFUNC9:28;
hence  dom ((Partial_Sums F) . n) = meet  {  (dom (F . k)) where k is Element of NAT : k <= n  }  ; ::_thesis: verum
end;

theorem Th11: :: MESFUN9C:11
for X being non empty set
for F being Functional_Sequence of X,REAL
for n being Nat st F is with_the_same_dom holds
dom ((Partial_Sums F) . n) = dom (F . 0)
proof
let X be non empty set ; ::_thesis: for F being Functional_Sequence of X,REAL
for n being Nat st F is with_the_same_dom holds
dom ((Partial_Sums F) . n) = dom (F . 0)
let F be Functional_Sequence of X,REAL; ::_thesis: for n being Nat st F is with_the_same_dom holds
dom ((Partial_Sums F) . n) = dom (F . 0)
let n be Nat; ::_thesis: ( F is with_the_same_dom implies dom ((Partial_Sums F) . n) = dom (F . 0) )
assume  F is with_the_same_dom ; ::_thesis: dom ((Partial_Sums F) . n) = dom (F . 0)
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  dom ((Partial_Sums F) . n) = dom (F . 0) ; ::_thesis: verum
end;

theorem Th12: :: MESFUN9C:12
for X being non empty set
for F being Functional_Sequence of X,REAL
for n being Nat
for x being Element of X
for D being set st F is with_the_same_dom & D c= dom (F . 0) & x in D holds
(Partial_Sums (F # x)) . n = ((Partial_Sums F) # x) . n
proof
let X be non empty set ; ::_thesis: for F being Functional_Sequence of X,REAL
for n being Nat
for x being Element of X
for D being set st F is with_the_same_dom & D c= dom (F . 0) & x in D holds
(Partial_Sums (F # x)) . n = ((Partial_Sums F) # x) . n
let F be Functional_Sequence of X,REAL; ::_thesis: for n being Nat
for x being Element of X
for D being set st F is with_the_same_dom & D c= dom (F . 0) & x in D holds
(Partial_Sums (F # x)) . n = ((Partial_Sums F) # x) . n
let n be Nat; ::_thesis: for x being Element of X
for D being set st F is with_the_same_dom & D c= dom (F . 0) & x in D holds
(Partial_Sums (F # x)) . n = ((Partial_Sums F) # x) . n
let x be Element of X; ::_thesis: for D being set st F is with_the_same_dom & D c= dom (F . 0) & x in D holds
(Partial_Sums (F # x)) . n = ((Partial_Sums F) # x) . n
let D be set ; ::_thesis: ( 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 )
assume  ( F is with_the_same_dom & D c= dom (F . 0) & x in D ) ; ::_thesis: (Partial_Sums (F # x)) . n = ((Partial_Sums F) # x) . n
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  R_EAL ((Partial_Sums (F # x)) . n) = ((R_EAL (Partial_Sums F)) # x) . n by Th7;
hence  (Partial_Sums (F # x)) . n = ((Partial_Sums F) # x) . n by MESFUN7C:1; ::_thesis: verum
end;

theorem Th13: :: MESFUN9C:13
for X being non empty set
for F being Functional_Sequence of X,REAL
for x being Element of X
for D being set st F is with_the_same_dom & D c= dom (F . 0) & x in D holds
( Partial_Sums (F # x) is convergent iff (Partial_Sums F) # x is convergent )
proof
let X be non empty set ; ::_thesis: for F being Functional_Sequence of X,REAL
for x being Element of X
for D being set st F is with_the_same_dom & D c= dom (F . 0) & x in D holds
( Partial_Sums (F # x) is convergent iff (Partial_Sums F) # x is convergent )
let F be Functional_Sequence of X,REAL; ::_thesis: for x being Element of X
for D being set st F is with_the_same_dom & D c= dom (F . 0) & x in D holds
( Partial_Sums (F # x) is convergent iff (Partial_Sums F) # x is convergent )
let x be Element of X; ::_thesis: for D being set st F is with_the_same_dom & D c= dom (F . 0) & x in D holds
( Partial_Sums (F # x) is convergent iff (Partial_Sums F) # x is convergent )
let D be set ; ::_thesis: ( 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 ) )
assume A1: ( F is with_the_same_dom & D c= dom (F . 0) & x in D ) ; ::_thesis: ( Partial_Sums (F # x) is convergent iff (Partial_Sums F) # x is convergent )
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  ::_thesis: ( (Partial_Sums F) # x is convergent implies Partial_Sums (F # x) is convergent )
assume  Partial_Sums (F # x) is convergent ; ::_thesis: (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; ::_thesis: verum
end;
assume  (Partial_Sums F) # x is convergent ; ::_thesis: 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; ::_thesis: verum
end;

theorem Th14: :: MESFUN9C:14
for X being non empty set
for F being Functional_Sequence of X,REAL
for f being PartFunc of X,REAL
for x being Element of X st F is with_the_same_dom & dom f c= dom (F . 0) & x in dom f & f . x = Sum (F # x) holds
f . x = lim ((Partial_Sums F) # x)
proof
let X be non empty set ; ::_thesis: for F being Functional_Sequence of X,REAL
for f being PartFunc of X,REAL
for x being Element of X st F is with_the_same_dom & dom f c= dom (F . 0) & x in dom f & f . x = Sum (F # x) holds
f . x = lim ((Partial_Sums F) # x)
let F be Functional_Sequence of X,REAL; ::_thesis: for f being PartFunc of X,REAL
for x being Element of X st F is with_the_same_dom & dom f c= dom (F . 0) & x in dom f & f . x = Sum (F # x) holds
f . x = lim ((Partial_Sums F) # x)
let f be PartFunc of X,REAL; ::_thesis: for x being Element of X st F is with_the_same_dom & dom f c= dom (F . 0) & x in dom f & f . x = Sum (F # x) holds
f . x = lim ((Partial_Sums F) # x)
let x be Element of X; ::_thesis: ( 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) )
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) ; ::_thesis: f . x = lim ((Partial_Sums F) # x)
A3: ( dom (Partial_Sums (F # x)) = NAT & dom ((Partial_Sums F) # x) = NAT ) by FUNCT_2:def_1;
 for n being set 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; ::_thesis: verum
end;

theorem Th15: :: MESFUN9C:15
for X being non empty set
for S being SigmaField of X
for F being Functional_Sequence of X,REAL
for n being Nat st ( for m being Nat holds F . m is_simple_func_in S ) holds
(Partial_Sums F) . n is_simple_func_in S
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for F being Functional_Sequence of X,REAL
for n being Nat st ( for m being Nat holds F . m is_simple_func_in S ) holds
(Partial_Sums F) . n is_simple_func_in S
let S be SigmaField of X; ::_thesis: for F being Functional_Sequence of X,REAL
for n being Nat st ( for m being Nat holds F . m is_simple_func_in S ) holds
(Partial_Sums F) . n is_simple_func_in S
let F be Functional_Sequence of X,REAL; ::_thesis: for n being Nat st ( for m being Nat holds F . m is_simple_func_in S ) holds
(Partial_Sums F) . n is_simple_func_in S
let n be Nat; ::_thesis: ( ( for m being Nat holds F . m is_simple_func_in S ) implies (Partial_Sums F) . n is_simple_func_in S )
assume A1: for m being Nat holds F . m is_simple_func_in S ; ::_thesis: (Partial_Sums F) . n is_simple_func_in S
 for m being Nat holds (R_EAL F) . m is_simple_func_in S
proof
let m be Nat; ::_thesis: (R_EAL F) . m is_simple_func_in S
 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 ; ::_thesis: verum
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; ::_thesis: verum
end;

theorem Th16: :: MESFUN9C:16
for X being non empty set
for S being SigmaField of X
for E being Element of S
for F being Functional_Sequence of X,REAL
for m being Nat st ( for n being Nat holds F . n is_measurable_on E ) holds
(Partial_Sums F) . m is_measurable_on E
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for E being Element of S
for F being Functional_Sequence of X,REAL
for m being Nat st ( for n being Nat holds F . n is_measurable_on E ) holds
(Partial_Sums F) . m is_measurable_on E
let S be SigmaField of X; ::_thesis: for E being Element of S
for F being Functional_Sequence of X,REAL
for m being Nat st ( for n being Nat holds F . n is_measurable_on E ) holds
(Partial_Sums F) . m is_measurable_on E
let E be Element of S; ::_thesis: for F being Functional_Sequence of X,REAL
for m being Nat st ( for n being Nat holds F . n is_measurable_on E ) holds
(Partial_Sums F) . m is_measurable_on E
let F be Functional_Sequence of X,REAL; ::_thesis: for m being Nat st ( for n being Nat holds F . n is_measurable_on E ) holds
(Partial_Sums F) . m is_measurable_on E
let m be Nat; ::_thesis: ( ( for n being Nat holds F . n is_measurable_on E ) implies (Partial_Sums F) . m is_measurable_on E )
set PF = Partial_Sums F;
defpred S1[ Nat] means (Partial_Sums F) . $1 is_measurable_on E;
assume A1: for n being Nat holds F . n is_measurable_on E ; ::_thesis: (Partial_Sums F) . m is_measurable_on E
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; ::_thesis: S1[k + 1]
 F . (k + 1) is_measurable_on E by A1;
then  ((Partial_Sums F) . k) + (F . (k + 1)) is_measurable_on E by A3, MESFUNC6:26;
hence  S1[k + 1] by Def2; ::_thesis: verum
end;
 (Partial_Sums F) . 0 = F . 0 by Def2;
then A4: S1[ 0 ] by A1;
 for k being Nat holds S1[k] from NAT_1:sch_2(A4, A2);
hence  (Partial_Sums F) . m is_measurable_on E ; ::_thesis: verum
end;

theorem Th17: :: MESFUN9C:17
for X being non empty set
for F being 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 ; ::_thesis: for F being Functional_Sequence of X,REAL st F is with_the_same_dom holds
Partial_Sums F is with_the_same_dom
let F be Functional_Sequence of X,REAL; ::_thesis: ( F is with_the_same_dom implies Partial_Sums F is with_the_same_dom )
assume A1: F is with_the_same_dom ; ::_thesis: Partial_Sums F is with_the_same_dom
let n, m be Nat; :: according to MESFUNC8:def_2 ::_thesis: dom ((Partial_Sums F) . n) = dom ((Partial_Sums F) . m)
 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; ::_thesis: verum
end;

theorem Th18: :: MESFUN9C:18
for X being non empty set
for S being SigmaField of X
for E being Element of S
for F being Functional_Sequence of X,REAL st dom (F . 0) = E & F is with_the_same_dom & ( for n being Nat holds (Partial_Sums F) . n is_measurable_on E ) & ( for x being Element of X st x in E holds
F # x is summable ) holds
lim (Partial_Sums F) is_measurable_on E
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for E being Element of S
for F being Functional_Sequence of X,REAL st dom (F . 0) = E & F is with_the_same_dom & ( for n being Nat holds (Partial_Sums F) . n is_measurable_on E ) & ( for x being Element of X st x in E holds
F # x is summable ) holds
lim (Partial_Sums F) is_measurable_on E
let S be SigmaField of X; ::_thesis: for E being Element of S
for F being Functional_Sequence of X,REAL st dom (F . 0) = E & F is with_the_same_dom & ( for n being Nat holds (Partial_Sums F) . n is_measurable_on E ) & ( for x being Element of X st x in E holds
F # x is summable ) holds
lim (Partial_Sums F) is_measurable_on E
let E be Element of S; ::_thesis: for F being Functional_Sequence of X,REAL st dom (F . 0) = E & F is with_the_same_dom & ( for n being Nat holds (Partial_Sums F) . n is_measurable_on E ) & ( for x being Element of X st x in E holds
F # x is summable ) holds
lim (Partial_Sums F) is_measurable_on E
let F be Functional_Sequence of X,REAL; ::_thesis: ( dom (F . 0) = E & F is with_the_same_dom & ( for n being Nat holds (Partial_Sums F) . n is_measurable_on E ) & ( for x being Element of X st x in E holds
F # x is summable ) implies lim (Partial_Sums F) is_measurable_on E )
assume that
A1: ( dom (F . 0) = E & F is with_the_same_dom ) and
A2: for n being Nat holds (Partial_Sums F) . n is_measurable_on E and
A3: for x being Element of X st x in E holds
F # x is summable ; ::_thesis: lim (Partial_Sums F) is_measurable_on E
A4: now__::_thesis:_for_x_being_Element_of_X_st_x_in_E_holds_
(Partial_Sums_F)_#_x_is_convergent
let x be Element of X; ::_thesis: ( x in E implies (Partial_Sums F) # x is convergent )
assume A5: x in E ; ::_thesis: (Partial_Sums F) # x is convergent
then  F # x is summable by A3;
then  Partial_Sums (F # x) is convergent by SERIES_1:def_2;
hence  (Partial_Sums F) # x is convergent by A1, A5, Th13; ::_thesis: verum
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  lim (Partial_Sums F) is_measurable_on E by A2, A4, MESFUN7C:21; ::_thesis: verum
end;

theorem Th19: :: MESFUN9C:19
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for F being Functional_Sequence of X,REAL st ( for n being Nat holds F . n is_integrable_on M ) holds
for m being Nat holds (Partial_Sums F) . m is_integrable_on M
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for F being Functional_Sequence of X,REAL st ( for n being Nat holds F . n is_integrable_on M ) holds
for m being Nat holds (Partial_Sums F) . m is_integrable_on M
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for F being Functional_Sequence of X,REAL st ( for n being Nat holds F . n is_integrable_on M ) holds
for m being Nat holds (Partial_Sums F) . m is_integrable_on M
let M be sigma_Measure of S; ::_thesis: for F being Functional_Sequence of X,REAL st ( for n being Nat holds F . n is_integrable_on M ) holds
for m being Nat holds (Partial_Sums F) . m is_integrable_on M
let F be Functional_Sequence of X,REAL; ::_thesis: ( ( for n being Nat holds F . n is_integrable_on M ) implies for m being Nat holds (Partial_Sums F) . m is_integrable_on M )
assume A1: for n being Nat holds F . n is_integrable_on M ; ::_thesis: for m being Nat holds (Partial_Sums F) . m is_integrable_on M
let m be Nat; ::_thesis: (Partial_Sums F) . m is_integrable_on M
 for n being Nat holds (R_EAL F) . n is_integrable_on M
proof
let n be Nat; ::_thesis: (R_EAL F) . n is_integrable_on M
 F . n is_integrable_on M by A1;
then  R_EAL (F . n) is_integrable_on M by MESFUNC6:def_4;
hence  (R_EAL F) . n is_integrable_on M ; ::_thesis: verum
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 by MESFUNC6:def_4; ::_thesis: verum
end;

begin


theorem Th20: :: MESFUN9C:20
for X being non empty set
for f being PartFunc of X,COMPLEX
for A being set holds
( (Re f) | A = Re (f | A) & (Im f) | A = Im (f | A) )
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,COMPLEX
for A being set holds
( (Re f) | A = Re (f | A) & (Im f) | A = Im (f | A) )
let f be PartFunc of X,COMPLEX; ::_thesis: for A being set holds
( (Re f) | A = Re (f | A) & (Im f) | A = Im (f | A) )
let A be set ; ::_thesis: ( (Re f) | A = Re (f | A) & (Im f) | A = Im (f | A) )
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__::_thesis:_for_x_being_set_st_x_in_dom_((Re_f)_|_A)_holds_
(Re_(f_|_A))_._x_=_((Re_f)_|_A)_._x
let x be set ; ::_thesis: ( x in dom ((Re f) | A) implies (Re (f | A)) . x = ((Re f) | A) . x )
assume A2: x in dom ((Re f) | A) ; ::_thesis: (Re (f | A)) . x = ((Re f) | A) . x
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 ; ::_thesis: verum
end;
hence  (Re f) | A = Re (f | A) by A1, FUNCT_1:2; ::_thesis: (Im f) | A = Im (f | A)
 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__::_thesis:_for_x_being_set_st_x_in_dom_((Im_f)_|_A)_holds_
(Im_(f_|_A))_._x_=_((Im_f)_|_A)_._x
let x be set ; ::_thesis: ( x in dom ((Im f) | A) implies (Im (f | A)) . x = ((Im f) | A) . x )
assume A7: x in dom ((Im f) | A) ; ::_thesis: (Im (f | A)) . x = ((Im f) | A) . x
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 ; ::_thesis: verum
end;
hence  (Im f) | A = Im (f | A) by A6, FUNCT_1:2; ::_thesis: verum
end;

Lm1:  for X being non empty set
for D being set
for F being Functional_Sequence of X,COMPLEX
for n being Nat holds
( (Re (F || D)) . n = ((Re F) . n) | D & (Im (F || D)) . n = ((Im F) . n) | D )
proof
let X be non empty set ; ::_thesis: for D being set
for F being Functional_Sequence of X,COMPLEX
for n being Nat holds
( (Re (F || D)) . n = ((Re F) . n) | D & (Im (F || D)) . n = ((Im F) . n) | D )
let D be set ; ::_thesis: for F being Functional_Sequence of X,COMPLEX
for n being Nat holds
( (Re (F || D)) . n = ((Re F) . n) | D & (Im (F || D)) . n = ((Im F) . n) | D )
let F be Functional_Sequence of X,COMPLEX; ::_thesis: for n being Nat holds
( (Re (F || D)) . n = ((Re F) . n) | D & (Im (F || D)) . n = ((Im F) . n) | D )
set G = F || D;
let n be Nat; ::_thesis: ( (Re (F || D)) . n = ((Re F) . n) | D & (Im (F || D)) . n = ((Im F) . n) | D )
 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 ((F || D) . n) = (Re (F || D)) . n & Im ((F || D) . n) = (Im (F || D)) . n ) by MESFUN7C:24;
hence  ( (Re (F || D)) . n = ((Re F) . n) | D & (Im (F || D)) . n = ((Im F) . n) | D ) by A1, A2, Def1; ::_thesis: verum
end;

theorem Th21: :: MESFUN9C:21
for X being non empty set
for D being set
for F being Functional_Sequence of X,COMPLEX holds Re (F || D) = (Re F) || D
proof
let X be non empty set ; ::_thesis: for D being set
for F being Functional_Sequence of X,COMPLEX holds Re (F || D) = (Re F) || D
let D be set ; ::_thesis: for F being Functional_Sequence of X,COMPLEX holds Re (F || D) = (Re F) || D
let F be Functional_Sequence of X,COMPLEX; ::_thesis: Re (F || D) = (Re F) || D
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: (Re (F || D)) . n = ((Re F) || D) . n
 (Re (F || D)) . n = ((Re F) . n) | D by Lm1;
hence  (Re (F || D)) . n = ((Re F) || D) . n by Def1; ::_thesis: verum
end;

theorem Th22: :: MESFUN9C:22
for X being non empty set
for D being set
for F being Functional_Sequence of X,COMPLEX holds Im (F || D) = (Im F) || D
proof
let X be non empty set ; ::_thesis: for D being set
for F being Functional_Sequence of X,COMPLEX holds Im (F || D) = (Im F) || D
let D be set ; ::_thesis: for F being Functional_Sequence of X,COMPLEX holds Im (F || D) = (Im F) || D
let F be Functional_Sequence of X,COMPLEX; ::_thesis: Im (F || D) = (Im F) || D
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: (Im (F || D)) . n = ((Im F) || D) . n
 (Im (F || D)) . n = ((Im F) . n) | D by Lm1;
hence  (Im (F || D)) . n = ((Im F) || D) . n by Def1; ::_thesis: verum
end;

theorem Th23: :: MESFUN9C:23
for X being non empty set
for x being Element of X
for D being set
for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & D c= dom (F . 0) & x in D & F # x is convergent holds
(F || D) # x is convergent
proof
let X be non empty set ; ::_thesis: for x being Element of X
for D being set
for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & D c= dom (F . 0) & x in D & F # x is convergent holds
(F || D) # x is convergent
let x be Element of X; ::_thesis: for D being set
for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & D c= dom (F . 0) & x in D & F # x is convergent holds
(F || D) # x is convergent
let D be set ; ::_thesis: for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & D c= dom (F . 0) & x in D & F # x is convergent holds
(F || D) # x is convergent
let F be Functional_Sequence of X,COMPLEX; ::_thesis: ( F is with_the_same_dom & D c= dom (F . 0) & x in D & F # x is convergent implies (F || D) # x is convergent )
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 ; ::_thesis: ( not F # x is convergent or (F || D) # x is convergent )
 Re (F || D) = (Re F) || D by Th21;
then A4: ( (Re F) # x is convergent implies (Re (F || D)) # 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 (F || D)) . 0) = D by Lm1;
then A5: dom ((F || D) . 0) = D by MESFUN7C:def_11;
 F || D is with_the_same_dom by A1, Th2;
then A6: ( (Re (F || D)) # x = Re ((F || D) # x) & (Im (F || D)) # x = Im ((F || D) # x) ) by A3, A5, MESFUN7C:23;
 Im (F || D) = (Im F) || D by Th22;
then A7: ( (Im F) # x is convergent implies (Im (F || D)) # 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  ( not F # x is convergent or (F || D) # x is convergent ) by A4, A7, A6, COMSEQ_3:42; ::_thesis: verum
end;

theorem Th24: :: MESFUN9C:24
for X being non empty set
for F being Functional_Sequence of X,COMPLEX holds
( F is with_the_same_dom iff Re F is with_the_same_dom )
proof
let X be non empty set ; ::_thesis: for F being Functional_Sequence of X,COMPLEX holds
( F is with_the_same_dom iff Re F is with_the_same_dom )
let F be Functional_Sequence of X,COMPLEX; ::_thesis: ( F is with_the_same_dom iff Re F is with_the_same_dom )
thus  ( F is with_the_same_dom implies Re F is with_the_same_dom ) ; ::_thesis: ( Re F is with_the_same_dom implies F is with_the_same_dom )
assume A1: Re F is with_the_same_dom ; ::_thesis: F is with_the_same_dom
now__::_thesis:_for_n,_m_being_Nat_holds_dom_(F_._n)_=_dom_(F_._m)
let n, m be Nat; ::_thesis: dom (F . n) = dom (F . m)
 ( 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, MESFUNC8:def_2; ::_thesis: verum
end;
hence  F is with_the_same_dom by MESFUNC8:def_2; ::_thesis: verum
end;

theorem Th25: :: MESFUN9C:25
for X being non empty set
for F being Functional_Sequence of X,COMPLEX holds
( Re F is with_the_same_dom iff Im F is with_the_same_dom )
proof
let X be non empty set ; ::_thesis: for F being Functional_Sequence of X,COMPLEX holds
( Re F is with_the_same_dom iff Im F is with_the_same_dom )
let F be Functional_Sequence of X,COMPLEX; ::_thesis: ( Re F is with_the_same_dom iff Im F is with_the_same_dom )
hereby  ::_thesis: ( Im F is with_the_same_dom implies Re F is with_the_same_dom )
assume  Re F is with_the_same_dom ; ::_thesis: Im F is with_the_same_dom
then  F is with_the_same_dom by Th24;
then  for n, m being 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 by MESFUNC8:def_2; ::_thesis: verum
end;
assume A1: Im F is with_the_same_dom ; ::_thesis: Re F is with_the_same_dom
now__::_thesis:_for_n,_m_being_Nat_holds_dom_(F_._n)_=_dom_(F_._m)
let n, m be Nat; ::_thesis: dom (F . n) = dom (F . m)
 ( 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, MESFUNC8:def_2; ::_thesis: verum
end;
then  F is with_the_same_dom by MESFUNC8:def_2;
hence  Re F is with_the_same_dom ; ::_thesis: verum
end;

theorem :: MESFUN9C:26
for X being non empty set
for D being set
for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & D = dom (F . 0) & ( for x being Element of X st x in D holds
F # x is convergent ) holds
(lim F) | D = lim (F || D)
proof
let X be non empty set ; ::_thesis: for D being set
for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & D = dom (F . 0) & ( for x being Element of X st x in D holds
F # x is convergent ) holds
(lim F) | D = lim (F || D)
let D be set ; ::_thesis: for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & D = dom (F . 0) & ( for x being Element of X st x in D holds
F # x is convergent ) holds
(lim F) | D = lim (F || D)
let F be Functional_Sequence of X,COMPLEX; ::_thesis: ( F is with_the_same_dom & D = dom (F . 0) & ( for x being Element of X st x in D holds
F # x is convergent ) implies (lim F) | D = lim (F || D) )
set G = F || D;
assume that
A1: F is with_the_same_dom and
A2: D = dom (F . 0) and
A3: for x being Element of X st x in D holds
F # x is convergent ; ::_thesis: (lim F) | D = lim (F || D)
A4: Re (F || D) = (Re F) || D by Th21;
A5: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_((F_||_D)_._0)_holds_
(F_||_D)_#_x_is_convergent
let x be Element of X; ::_thesis: ( x in dom ((F || D) . 0) implies (F || D) # x is convergent )
 dom ((F . 0) | D) = D by A2, RELAT_1:62;
then A6: dom ((F || D) . 0) = D by Def1;
assume A7: x in dom ((F || D) . 0) ; ::_thesis: (F || D) # x is convergent
then  F # x is convergent by A3, A6;
hence  (F || D) # x is convergent by A1, A2, A7, A6, Th23; ::_thesis: verum
end;
A8: for x being Element of X st x in D holds
(Re F) # x is convergent
proof
let x be Element of X; ::_thesis: ( x in D implies (Re F) # x is convergent )
assume A9: x in D ; ::_thesis: (Re F) # x is convergent
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; ::_thesis: verum
end;
 D c= dom ((Re F) . 0) by A2, MESFUN7C:def_11;
then  (lim (Re F)) | D = lim (Re (F || D)) by A4, A8, Th3;
then A10: (Re (lim F)) | D = lim (Re (F || D)) by A1, A2, A3, MESFUN7C:25;
A11: F || D is with_the_same_dom by A1, Th2;
then  lim (Re (F || D)) = Re (lim (F || D)) by A5, MESFUN7C:25;
then A12: Re ((lim F) | D) = Re (lim (F || D)) by A10, Th20;
A13: for x being Element of X st x in D holds
(Im F) # x is convergent
proof
let x be Element of X; ::_thesis: ( x in D implies (Im F) # x is convergent )
assume A14: x in D ; ::_thesis: (Im F) # x is convergent
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; ::_thesis: verum
end;
A15: Im (F || D) = (Im F) || D by Th22;
 D c= dom ((Im F) . 0) by A2, MESFUN7C:def_12;
then  (lim (Im F)) | D = lim (Im (F || D)) by A15, A13, Th3;
then A16: (Im (lim F)) | D = lim (Im (F || D)) by A1, A2, A3, MESFUN7C:25;
 lim (Im (F || D)) = Im (lim (F || D)) by A11, A5, MESFUN7C:25;
then A17: Im ((lim F) | D) = Im (lim (F || D)) by A16, Th20;
thus  lim (F || D) = (Re (lim (F || D))) + (<i> (#) (Im (lim (F || D)))) by MESFUN6C:8
.= (lim F) | D by A12, A17, MESFUN6C:8 ; ::_thesis: verum
end;

theorem :: MESFUN9C:27
for X being non empty set
for S being SigmaField of X
for E being Element of S
for n being Nat
for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & E c= dom (F . 0) & ( for m being Nat holds F . m is_measurable_on E ) holds
(F || E) . n is_measurable_on E
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for E being Element of S
for n being Nat
for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & E c= dom (F . 0) & ( for m being Nat holds F . m is_measurable_on E ) holds
(F || E) . n is_measurable_on E
let S be SigmaField of X; ::_thesis: for E being Element of S
for n being Nat
for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & E c= dom (F . 0) & ( for m being Nat holds F . m is_measurable_on E ) holds
(F || E) . n is_measurable_on E
let E be Element of S; ::_thesis: for n being Nat
for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & E c= dom (F . 0) & ( for m being Nat holds F . m is_measurable_on E ) holds
(F || E) . n is_measurable_on E
let n be Nat; ::_thesis: for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & E c= dom (F . 0) & ( for m being Nat holds F . m is_measurable_on E ) holds
(F || E) . n is_measurable_on E
let F be Functional_Sequence of X,COMPLEX; ::_thesis: ( F is with_the_same_dom & E c= dom (F . 0) & ( for m being Nat holds F . m is_measurable_on E ) implies (F || E) . n is_measurable_on E )
set G = F || E;
A1: Re (F || E) = (Re F) || E by Th21;
A2: Im (F || E) = (Im F) || E by Th22;
assume  F is with_the_same_dom ; ::_thesis: ( not E c= dom (F . 0) or ex m being Nat st not F . m is_measurable_on E or (F || E) . n is_measurable_on E )
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) ; ::_thesis: ( ex m being Nat st not F . m is_measurable_on E or (F || E) . n is_measurable_on E )
assume A6: for m being Nat holds F . m is_measurable_on E ; ::_thesis: (F || E) . n is_measurable_on E
A7: for m being Nat holds
( (Re F) . m is_measurable_on E & (Im F) . m is_measurable_on E )
proof
let m be Nat; ::_thesis: ( (Re F) . m is_measurable_on E & (Im F) . m is_measurable_on E )
 F . m is_measurable_on E by A6;
then  ( Re (F . m) is_measurable_on E & Im (F . m) is_measurable_on E ) by MESFUN6C:def_1;
hence  ( (Re F) . m is_measurable_on E & (Im F) . m is_measurable_on E ) by MESFUN7C:24; ::_thesis: verum
end;
 E c= dom ((Im F) . 0) by A5, MESFUN7C:def_12;
then  (Im (F || E)) . n is_measurable_on E by A4, A2, A7, Th4;
then A8: Im ((F || E) . n) is_measurable_on E by MESFUN7C:24;
 E c= dom ((Re F) . 0) by A5, MESFUN7C:def_11;
then  (Re (F || E)) . n is_measurable_on E by A3, A1, A7, Th4;
then  Re ((F || E) . n) is_measurable_on E by MESFUN7C:24;
hence  (F || E) . n is_measurable_on E by A8, MESFUN6C:def_1; ::_thesis: verum
end;

theorem :: MESFUN9C:28
for X being non empty set
for S being SigmaField of X
for E being Element of S
for F being Functional_Sequence of X,COMPLEX st E c= dom (F . 0) & F is with_the_same_dom & ( for x being Element of X st x in E holds
F # x is summable ) holds
for x being Element of X st x in E holds
(F || E) # x is summable
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for E being Element of S
for F being Functional_Sequence of X,COMPLEX st E c= dom (F . 0) & F is with_the_same_dom & ( for x being Element of X st x in E holds
F # x is summable ) holds
for x being Element of X st x in E holds
(F || E) # x is summable
let S be SigmaField of X; ::_thesis: for E being Element of S
for F being Functional_Sequence of X,COMPLEX st E c= dom (F . 0) & F is with_the_same_dom & ( for x being Element of X st x in E holds
F # x is summable ) holds
for x being Element of X st x in E holds
(F || E) # x is summable
let E be Element of S; ::_thesis: for F being Functional_Sequence of X,COMPLEX st E c= dom (F . 0) & F is with_the_same_dom & ( for x being Element of X st x in E holds
F # x is summable ) holds
for x being Element of X st x in E holds
(F || E) # x is summable
let F be Functional_Sequence of X,COMPLEX; ::_thesis: ( E c= dom (F . 0) & F is with_the_same_dom & ( for x being Element of X st x in E holds
F # x is summable ) implies for x being Element of X st x in E holds
(F || E) # x is summable )
set G = F || E;
assume that
A1: E c= dom (F . 0) and
A2: F is with_the_same_dom and
A3: for x being Element of X st x in E holds
F # x is summable ; ::_thesis: for x being Element of X st x in E holds
(F || E) # x is summable
A4: F || E is with_the_same_dom by A2, Th2;
A5: for x being Element of X st x in E holds
(Im F) # x is summable
proof
let x be Element of X; ::_thesis: ( x in E implies (Im F) # x is summable )
assume A6: x in E ; ::_thesis: (Im F) # x is summable
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; ::_thesis: verum
end;
A7: for x being Element of X st x in E holds
(Re F) # x is summable
proof
let x be Element of X; ::_thesis: ( x in E implies (Re F) # x is summable )
assume A8: x in E ; ::_thesis: (Re F) # x is summable
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; ::_thesis: verum
end;
hereby  ::_thesis: verum
let x be Element of X; ::_thesis: ( x in E implies (F || E) # x is summable )
assume A9: x in E ; ::_thesis: (F || E) # x is summable
 (F || E) . 0 = (F . 0) | E by Def1;
then A10: x in dom ((F || E) . 0) by A1, A9, RELAT_1:62;
 Im (F || E) = (Im F) || E by Th22;
then  (Im (F || E)) # x is summable by A5, A9, Th6;
then A11: Im ((F || E) # x) is summable by A4, A10, MESFUN7C:23;
 Re (F || E) = (Re F) || E by Th21;
then  (Re (F || E)) # x is summable by A7, A9, Th6;
then  Re ((F || E) # x) is summable by A4, A10, MESFUN7C:23;
hence  (F || E) # x is summable by A11, COMSEQ_3:57; ::_thesis: verum
end;
end;

definition
let X be non empty set ;
let F be Functional_Sequence of X,COMPLEX;
func Partial_Sums F ->  Functional_Sequence of X,COMPLEX means :Def3: :: MESFUN9C:def 3
( it . 0 = F . 0 & ( for n being Nat holds it . (n + 1) = (it . n) + (F . (n + 1)) ) );
existence
 ex b1 being Functional_Sequence of X,COMPLEX st
( b1 . 0 = F . 0 & ( for n being Nat holds b1 . (n + 1) = (b1 . n) + (F . (n + 1)) ) )
proof
defpred S1[ Element of NAT , set , set ] means ( ( $2 is not PartFunc of X,COMPLEX & $3 = F . $1 ) or ( $2 is PartFunc of X,COMPLEX & ( for F2 being PartFunc of X,COMPLEX st F2 = $2 holds
$3 = F2 + (F . ($1 + 1)) ) ) );
A1: for n being Element of NAT
for x being set ex y being set st S1[n,x,y]
proof
let n be Element of NAT ; ::_thesis: for x being set ex y being set st S1[n,x,y]
let x be set ; ::_thesis: ex y being set st S1[n,x,y]
now__::_thesis:_(_x_is_PartFunc_of_X,COMPLEX_implies_ex_y_being_Element_of_K6(K7(X,COMPLEX))_st_
(_(_x_is_not_PartFunc_of_X,COMPLEX_&_y_=_F_._n_)_or_(_x_is_PartFunc_of_X,COMPLEX_&_(_for_F2_being_PartFunc_of_X,COMPLEX_st_F2_=_x_holds_
y_=_F2_+_(F_._(n_+_1))_)_)_)_)
assume  x is PartFunc of X,COMPLEX ; ::_thesis: ex y being Element of K6(K7(X,COMPLEX)) st
( ( x is not PartFunc of X,COMPLEX & y = F . n ) or ( x is PartFunc of X,COMPLEX & ( for F2 being PartFunc of X,COMPLEX st F2 = x holds
y = F2 + (F . (n + 1)) ) ) )
then reconsider G2 = x as PartFunc of X,COMPLEX ;
take y = G2 + (F . (n + 1)); ::_thesis: ( ( x is not PartFunc of X,COMPLEX & y = F . n ) or ( x is PartFunc of X,COMPLEX & ( for F2 being PartFunc of X,COMPLEX st F2 = x holds
y = F2 + (F . (n + 1)) ) ) )
thus  ( ( x is not PartFunc of X,COMPLEX & y = F . n ) or ( x is PartFunc of X,COMPLEX & ( for F2 being PartFunc of X,COMPLEX st F2 = x holds
y = F2 + (F . (n + 1)) ) ) ) ; ::_thesis: verum
end;
hence  ex y being set st S1[n,x,y] ; ::_thesis: verum
end;
consider IT being Function such that
A2: ( dom IT = NAT & IT . 0 = F . 0 & ( for n being Element of NAT holds S1[n,IT . n,IT . (n + 1)] ) ) from RECDEF_1:sch_1(A1);
now__::_thesis:_for_f_being_set_st_f_in_rng_IT_holds_
f_in_PFuncs_(X,COMPLEX)
defpred S2[ Element of NAT ] means IT . $1 is PartFunc of X,COMPLEX;
let f be set ; ::_thesis: ( f in rng IT implies f in PFuncs (X,COMPLEX) )
assume  f in rng IT ; ::_thesis: f in PFuncs (X,COMPLEX)
then consider m being set  such that
A3: m in dom IT and
A4: f = IT . m by FUNCT_1:def_3;
reconsider m = m as Element of NAT by A2, A3;
A5: for n being Element of NAT st S2[n] holds
S2[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] )
assume  S2[n] ; ::_thesis: S2[n + 1]
then reconsider F2 = IT . n as PartFunc of X,COMPLEX ;
 IT . (n + 1) = F2 + (F . (n + 1)) by A2;
hence  S2[n + 1] ; ::_thesis: verum
end;
A6: S2[ 0 ] by A2;
 for n being Element of NAT holds S2[n] from NAT_1:sch_1(A6, A5);
then  IT . m is PartFunc of X,COMPLEX ;
hence  f in PFuncs (X,COMPLEX) by A4, PARTFUN1:45; ::_thesis: verum
end;
then  rng IT c= PFuncs (X,COMPLEX) by TARSKI:def_3;
then reconsider IT = IT as Functional_Sequence of X,COMPLEX by A2, FUNCT_2:def_1, RELSET_1:4;
take  IT ; ::_thesis: ( IT . 0 = F . 0 & ( for n being Nat holds IT . (n + 1) = (IT . n) + (F . (n + 1)) ) )
 for n being Nat holds IT . (n + 1) = (IT . n) + (F . (n + 1))
proof
let n be Nat; ::_thesis: IT . (n + 1) = (IT . n) + (F . (n + 1))
reconsider m = n as Element of NAT by ORDINAL1:def_12;
 IT . (m + 1) = (IT . m) + (F . (m + 1)) by A2;
hence  IT . (n + 1) = (IT . n) + (F . (n + 1)) ; ::_thesis: verum
end;
hence  ( IT . 0 = F . 0 & ( for n being Nat holds IT . (n + 1) = (IT . n) + (F . (n + 1)) ) ) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Functional_Sequence of X,COMPLEX st b1 . 0 = F . 0 & ( for n being Nat holds b1 . (n + 1) = (b1 . n) + (F . (n + 1)) ) & b2 . 0 = F . 0 & ( for n being Nat holds b2 . (n + 1) = (b2 . n) + (F . (n + 1)) ) holds
b1 = b2
proof
let PS1, PS2 be Functional_Sequence of X,COMPLEX; ::_thesis: ( PS1 . 0 = F . 0 & ( for n being Nat holds PS1 . (n + 1) = (PS1 . n) + (F . (n + 1)) ) & PS2 . 0 = F . 0 & ( for n being Nat holds PS2 . (n + 1) = (PS2 . n) + (F . (n + 1)) ) implies PS1 = PS2 )
assume that
A7: PS1 . 0 = F . 0 and
A8: for n being Nat holds PS1 . (n + 1) = (PS1 . n) + (F . (n + 1)) and
A9: PS2 . 0 = F . 0 and
A10: for n being Nat holds PS2 . (n + 1) = (PS2 . n) + (F . (n + 1)) ; ::_thesis: PS1 = PS2
defpred S1[ Nat] means PS1 . $1 = PS2 . $1;
A11: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A12: S1[n] ; ::_thesis: S1[n + 1]
 PS1 . (n + 1) = (PS1 . n) + (F . (n + 1)) by A8;
hence  PS1 . (n + 1) = PS2 . (n + 1) by A10, A12; ::_thesis: verum
end;
A13: S1[ 0 ] by A7, A9;
 for n being Nat holds S1[n] from NAT_1:sch_2(A13, A11);
then  for m being Element of NAT holds PS1 . m = PS2 . m ;
hence  PS1 = PS2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines Partial_Sums MESFUN9C:def_3_:_
 for X being non empty set
for F, b3 being Functional_Sequence of X,COMPLEX holds
( b3 = Partial_Sums F iff ( b3 . 0 = F . 0 & ( for n being Nat holds b3 . (n + 1) = (b3 . n) + (F . (n + 1)) ) ) );

theorem Th29: :: MESFUN9C:29
for X being non empty set
for F being Functional_Sequence of X,COMPLEX holds
( Partial_Sums (Re F) = Re (Partial_Sums F) & Partial_Sums (Im F) = Im (Partial_Sums F) )
proof
let X be non empty set ; ::_thesis: for F being Functional_Sequence of X,COMPLEX holds
( Partial_Sums (Re F) = Re (Partial_Sums F) & Partial_Sums (Im F) = Im (Partial_Sums F) )
let F be Functional_Sequence of X,COMPLEX; ::_thesis: ( Partial_Sums (Re F) = Re (Partial_Sums F) & Partial_Sums (Im F) = Im (Partial_Sums F) )
defpred S1[ Element of NAT ] means (Partial_Sums (Re F)) . $1 = (Re (Partial_Sums F)) . $1;
defpred S2[ Element of NAT ] means (Partial_Sums (Im F)) . $1 = (Im (Partial_Sums F)) . $1;
A1: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume  S1[k] ; ::_thesis: S1[k + 1]
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  S1[k + 1] by MESFUN7C:24; ::_thesis: verum
end;
A2: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] )
assume  S2[k] ; ::_thesis: S2[k + 1]
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  S2[k + 1] by MESFUN7C:24; ::_thesis: verum
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: S2[ 0 ] by MESFUN7C:24;
A4: for i being Element of NAT holds S2[i] from NAT_1:sch_1(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: S1[ 0 ] by MESFUN7C:24;
 for i being Element of NAT holds S1[i] from NAT_1:sch_1(A5, A1);
hence  ( Partial_Sums (Re F) = Re (Partial_Sums F) & Partial_Sums (Im F) = Im (Partial_Sums F) ) by A4, FUNCT_2:63; ::_thesis: verum
end;

theorem :: MESFUN9C:30
for X being non empty set
for n, m being Nat
for z being set
for F being Functional_Sequence of X,COMPLEX st z in dom ((Partial_Sums F) . n) & m <= n holds
( z in dom ((Partial_Sums F) . m) & z in dom (F . m) )
proof
let X be non empty set ; ::_thesis: for n, m being Nat
for z being set
for F being Functional_Sequence of X,COMPLEX st z in dom ((Partial_Sums F) . n) & m <= n holds
( z in dom ((Partial_Sums F) . m) & z in dom (F . m) )
let n, m be Nat; ::_thesis: for z being set
for F being Functional_Sequence of X,COMPLEX st z in dom ((Partial_Sums F) . n) & m <= n holds
( z in dom ((Partial_Sums F) . m) & z in dom (F . m) )
let z be set ; ::_thesis: for F being Functional_Sequence of X,COMPLEX st z in dom ((Partial_Sums F) . n) & m <= n holds
( z in dom ((Partial_Sums F) . m) & z in dom (F . m) )
let F be Functional_Sequence of X,COMPLEX; ::_thesis: ( z in dom ((Partial_Sums F) . n) & m <= n implies ( z in dom ((Partial_Sums F) . m) & z in dom (F . m) ) )
assume A1: ( z in dom ((Partial_Sums F) . n) & m <= n ) ; ::_thesis: ( z in dom ((Partial_Sums F) . m) & z in dom (F . m) )
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; ::_thesis: z in dom (F . m)
 z in dom ((Re F) . m) by A1, A2, Th8;
hence  z in dom (F . m) by MESFUN7C:def_11; ::_thesis: verum
end;

theorem :: MESFUN9C:31
for X being non empty set
for n being Nat
for F being Functional_Sequence of X,COMPLEX holds dom ((Partial_Sums F) . n) = meet  {  (dom (F . k)) where k is Element of NAT : k <= n  }
proof
let X be non empty set ; ::_thesis: for n being Nat
for F being Functional_Sequence of X,COMPLEX holds dom ((Partial_Sums F) . n) = meet  {  (dom (F . k)) where k is Element of NAT : k <= n  }
let n be Nat; ::_thesis: for F being Functional_Sequence of X,COMPLEX holds dom ((Partial_Sums F) . n) = meet  {  (dom (F . k)) where k is Element of NAT : k <= n  }
let F be Functional_Sequence of X,COMPLEX; ::_thesis: dom ((Partial_Sums F) . n) = meet  {  (dom (F . k)) where k is Element of NAT : k <= n  }
now__::_thesis:_for_A_being_set_st_A_in__{__(dom_((Re_F)_._k))_where_k_is_Element_of_NAT_:_k_<=_n__}__holds_
A_in__{__(dom_(F_._k))_where_k_is_Element_of_NAT_:_k_<=_n__}_
let A be set ; ::_thesis: ( A in  {  (dom ((Re F) . k)) where k is Element of NAT : k <= n  }  implies A in  {  (dom (F . k)) where k is Element of NAT : k <= n  }  )
assume  A in  {  (dom ((Re F) . k)) where k is Element of NAT : k <= n  }  ; ::_thesis: A in  {  (dom (F . k)) where k is Element of NAT : k <= n  }
then consider i being 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 is Element of NAT : k <= n  }  by A2; ::_thesis: verum
end;
then A3:  {  (dom ((Re F) . k)) where k is Element of NAT : k <= n  }  c=  {  (dom (F . k)) where k is Element of NAT : k <= n  }  by TARSKI:def_3;
now__::_thesis:_for_A_being_set_st_A_in__{__(dom_(F_._k))_where_k_is_Element_of_NAT_:_k_<=_n__}__holds_
A_in__{__(dom_((Re_F)_._k))_where_k_is_Element_of_NAT_:_k_<=_n__}_
let A be set ; ::_thesis: ( A in  {  (dom (F . k)) where k is Element of NAT : k <= n  }  implies A in  {  (dom ((Re F) . k)) where k is Element of NAT : k <= n  }  )
assume  A in  {  (dom (F . k)) where k is Element of NAT : k <= n  }  ; ::_thesis: A in  {  (dom ((Re F) . k)) where k is Element of NAT : k <= n  }
then consider i being 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 is Element of NAT : k <= n  }  by A5; ::_thesis: verum
end;
then A6:  {  (dom (F . k)) where k is Element of NAT : k <= n  }  c=  {  (dom ((Re F) . k)) where k is 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 is Element of NAT : k <= n  }  by Th10;
hence  dom ((Partial_Sums F) . n) = meet  {  (dom (F . k)) where k is Element of NAT : k <= n  }  by A7, A3, A6, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th32: :: MESFUN9C:32
for X being non empty set
for n being Nat
for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom holds
dom ((Partial_Sums F) . n) = dom (F . 0)
proof
let X be non empty set ; ::_thesis: for n being Nat
for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom holds
dom ((Partial_Sums F) . n) = dom (F . 0)
let n be Nat; ::_thesis: for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom holds
dom ((Partial_Sums F) . n) = dom (F . 0)
let F be Functional_Sequence of X,COMPLEX; ::_thesis: ( F is with_the_same_dom implies dom ((Partial_Sums F) . n) = dom (F . 0) )
assume  F is with_the_same_dom ; ::_thesis: dom ((Partial_Sums F) . n) = dom (F . 0)
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; ::_thesis: verum
end;

theorem :: MESFUN9C:33
for X being non empty set
for n being Nat
for x being Element of X
for D being set
for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & D c= dom (F . 0) & x in D holds
(Partial_Sums (F # x)) . n = ((Partial_Sums F) # x) . n
proof
let X be non empty set ; ::_thesis: for n being Nat
for x being Element of X
for D being set
for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & D c= dom (F . 0) & x in D holds
(Partial_Sums (F # x)) . n = ((Partial_Sums F) # x) . n
let n be Nat; ::_thesis: for x being Element of X
for D being set
for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & D c= dom (F . 0) & x in D holds
(Partial_Sums (F # x)) . n = ((Partial_Sums F) # x) . n
let x be Element of X; ::_thesis: for D being set
for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & D c= dom (F . 0) & x in D holds
(Partial_Sums (F # x)) . n = ((Partial_Sums F) # x) . n
let D be set ; ::_thesis: for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & D c= dom (F . 0) & x in D holds
(Partial_Sums (F # x)) . n = ((Partial_Sums F) # x) . n
let F be Functional_Sequence of X,COMPLEX; ::_thesis: ( 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 )
assume that
A1: F is with_the_same_dom and
A2: D c= dom (F . 0) and
A3: x in D ; ::_thesis: (Partial_Sums (F # x)) . n = ((Partial_Sums F) # x) . n
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: n is Element of NAT by ORDINAL1:def_12;
then A11: 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, A10, 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 ;
A12: x in dom (Im ((Partial_Sums F) . n)) by A5, COMSEQ_3:def_4;
A13: Im ((Partial_Sums (F # x)) . n) = (Im (Partial_Sums (F # x))) . n by A10, 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, A10, 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 A12, 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 A11, A13, COMPLEX1:13 ; ::_thesis: verum
end;

theorem Th34: :: MESFUN9C:34
for X being non empty set
for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom holds
Partial_Sums F is with_the_same_dom
proof
let X be non empty set ; ::_thesis: for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom holds
Partial_Sums F is with_the_same_dom
let F be Functional_Sequence of X,COMPLEX; ::_thesis: ( F is with_the_same_dom implies Partial_Sums F is with_the_same_dom )
assume  F is with_the_same_dom ; ::_thesis: Partial_Sums 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; ::_thesis: verum
end;

theorem Th35: :: MESFUN9C:35
for X being non empty set
for x being Element of X
for D being set
for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & D c= dom (F . 0) & x in D holds
( Partial_Sums (F # x) is convergent iff (Partial_Sums F) # x is convergent )
proof
let X be non empty set ; ::_thesis: for x being Element of X
for D being set
for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & D c= dom (F . 0) & x in D holds
( Partial_Sums (F # x) is convergent iff (Partial_Sums F) # x is convergent )
let x be Element of X; ::_thesis: for D being set
for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & D c= dom (F . 0) & x in D holds
( Partial_Sums (F # x) is convergent iff (Partial_Sums F) # x is convergent )
let D be set ; ::_thesis: for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & D c= dom (F . 0) & x in D holds
( Partial_Sums (F # x) is convergent iff (Partial_Sums F) # x is convergent )
let F be Functional_Sequence of X,COMPLEX; ::_thesis: ( 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 ) )
assume that
A1: F is with_the_same_dom and
A2: D c= dom (F . 0) and
A3: x in D ; ::_thesis: ( Partial_Sums (F # x) is convergent iff (Partial_Sums F) # x is convergent )
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  ::_thesis: ( (Partial_Sums F) # x is convergent implies Partial_Sums (F # x) is convergent )
assume A9: Partial_Sums (F # x) is convergent ; ::_thesis: (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; ::_thesis: verum
end;
assume A11: (Partial_Sums F) # x is convergent ; ::_thesis: 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; ::_thesis: verum
end;

theorem :: MESFUN9C:36
for X being non empty set
for x being Element of X
for F being Functional_Sequence of X,COMPLEX
for f being PartFunc of X,COMPLEX st 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) holds
f . x = lim ((Partial_Sums F) # x)
proof
let X be non empty set ; ::_thesis: for x being Element of X
for F being Functional_Sequence of X,COMPLEX
for f being PartFunc of X,COMPLEX st 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) holds
f . x = lim ((Partial_Sums F) # x)
let x be Element of X; ::_thesis: for F being Functional_Sequence of X,COMPLEX
for f being PartFunc of X,COMPLEX st 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) holds
f . x = lim ((Partial_Sums F) # x)
let F be Functional_Sequence of X,COMPLEX; ::_thesis: for f being PartFunc of X,COMPLEX st 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) holds
f . x = lim ((Partial_Sums F) # x)
let f be PartFunc of X,COMPLEX; ::_thesis: ( 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) )
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) ; ::_thesis: f . x = lim ((Partial_Sums 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 ; ::_thesis: verum
end;

theorem :: MESFUN9C:37
for X being non empty set
for S being SigmaField of X
for n being Nat
for F being Functional_Sequence of X,COMPLEX st ( for m being Nat holds F . m is_simple_func_in S ) holds
(Partial_Sums F) . n is_simple_func_in S
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for n being Nat
for F being Functional_Sequence of X,COMPLEX st ( for m being Nat holds F . m is_simple_func_in S ) holds
(Partial_Sums F) . n is_simple_func_in S
let S be SigmaField of X; ::_thesis: for n being Nat
for F being Functional_Sequence of X,COMPLEX st ( for m being Nat holds F . m is_simple_func_in S ) holds
(Partial_Sums F) . n is_simple_func_in S
let n be Nat; ::_thesis: for F being Functional_Sequence of X,COMPLEX st ( for m being Nat holds F . m is_simple_func_in S ) holds
(Partial_Sums F) . n is_simple_func_in S
let F be Functional_Sequence of X,COMPLEX; ::_thesis: ( ( for m being Nat holds F . m is_simple_func_in S ) implies (Partial_Sums F) . n is_simple_func_in S )
assume A1: for m being Nat holds F . m is_simple_func_in S ; ::_thesis: (Partial_Sums F) . n is_simple_func_in S
 for m being Nat holds (Im F) . m is_simple_func_in S
proof
let m be Nat; ::_thesis: (Im F) . m is_simple_func_in S
 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; ::_thesis: verum
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 being Nat holds (Re F) . m is_simple_func_in S
proof
let m be Nat; ::_thesis: (Re F) . m is_simple_func_in S
 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; ::_thesis: verum
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; ::_thesis: verum
end;

Lm2:  for X being non empty set
for S being SigmaField of X
for E being Element of S
for m being Nat
for F being Functional_Sequence of X,COMPLEX st ( for n being Nat holds F . n is_measurable_on E ) holds
( (Re F) . m is_measurable_on E & (Im F) . m is_measurable_on E )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for E being Element of S
for m being Nat
for F being Functional_Sequence of X,COMPLEX st ( for n being Nat holds F . n is_measurable_on E ) holds
( (Re F) . m is_measurable_on E & (Im F) . m is_measurable_on E )
let S be SigmaField of X; ::_thesis: for E being Element of S
for m being Nat
for F being Functional_Sequence of X,COMPLEX st ( for n being Nat holds F . n is_measurable_on E ) holds
( (Re F) . m is_measurable_on E & (Im F) . m is_measurable_on E )
let E be Element of S; ::_thesis: for m being Nat
for F being Functional_Sequence of X,COMPLEX st ( for n being Nat holds F . n is_measurable_on E ) holds
( (Re F) . m is_measurable_on E & (Im F) . m is_measurable_on E )
let m be Nat; ::_thesis: for F being Functional_Sequence of X,COMPLEX st ( for n being Nat holds F . n is_measurable_on E ) holds
( (Re F) . m is_measurable_on E & (Im F) . m is_measurable_on E )
let F be Functional_Sequence of X,COMPLEX; ::_thesis: ( ( for n being Nat holds F . n is_measurable_on E ) implies ( (Re F) . m is_measurable_on E & (Im F) . m is_measurable_on E ) )
assume  for n being Nat holds F . n is_measurable_on E ; ::_thesis: ( (Re F) . m is_measurable_on E & (Im F) . m is_measurable_on E )
then  F . m is_measurable_on E ;
then  ( Re (F . m) is_measurable_on E & Im (F . m) is_measurable_on E ) by MESFUN6C:def_1;
hence  ( (Re F) . m is_measurable_on E & (Im F) . m is_measurable_on E ) by MESFUN7C:24; ::_thesis: verum
end;

theorem :: MESFUN9C:38
for X being non empty set
for S being SigmaField of X
for E being Element of S
for m being Nat
for F being Functional_Sequence of X,COMPLEX st ( for n being Nat holds F . n is_measurable_on E ) holds
(Partial_Sums F) . m is_measurable_on E
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for E being Element of S
for m being Nat
for F being Functional_Sequence of X,COMPLEX st ( for n being Nat holds F . n is_measurable_on E ) holds
(Partial_Sums F) . m is_measurable_on E
let S be SigmaField of X; ::_thesis: for E being Element of S
for m being Nat
for F being Functional_Sequence of X,COMPLEX st ( for n being Nat holds F . n is_measurable_on E ) holds
(Partial_Sums F) . m is_measurable_on E
let E be Element of S; ::_thesis: for m being Nat
for F being Functional_Sequence of X,COMPLEX st ( for n being Nat holds F . n is_measurable_on E ) holds
(Partial_Sums F) . m is_measurable_on E
let m be Nat; ::_thesis: for F being Functional_Sequence of X,COMPLEX st ( for n being Nat holds F . n is_measurable_on E ) holds
(Partial_Sums F) . m is_measurable_on E
let F be Functional_Sequence of X,COMPLEX; ::_thesis: ( ( for n being Nat holds F . n is_measurable_on E ) implies (Partial_Sums F) . m is_measurable_on E )
assume A1: for n being Nat holds F . n is_measurable_on E ; ::_thesis: (Partial_Sums F) . m is_measurable_on E
then  for n being Nat holds (Im F) . n is_measurable_on E by Lm2;
then  (Partial_Sums (Im F)) . m is_measurable_on E by Th16;
then  (Im (Partial_Sums F)) . m is_measurable_on E by Th29;
then A2: Im ((Partial_Sums F) . m) is_measurable_on E by MESFUN7C:24;
 for n being Nat holds (Re F) . n is_measurable_on E by A1, Lm2;
then  (Partial_Sums (Re F)) . m is_measurable_on E by Th16;
then  (Re (Partial_Sums F)) . m is_measurable_on E by Th29;
then  Re ((Partial_Sums F) . m) is_measurable_on E by MESFUN7C:24;
hence  (Partial_Sums F) . m is_measurable_on E by A2, MESFUN6C:def_1; ::_thesis: verum
end;

theorem :: MESFUN9C:39
for X being non empty set
for S being SigmaField of X
for E being Element of S
for F being Functional_Sequence of X,COMPLEX st dom (F . 0) = E & F is with_the_same_dom & ( for n being Nat holds (Partial_Sums F) . n is_measurable_on E ) & ( for x being Element of X st x in E holds
F # x is summable ) holds
lim (Partial_Sums F) is_measurable_on E
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for E being Element of S
for F being Functional_Sequence of X,COMPLEX st dom (F . 0) = E & F is with_the_same_dom & ( for n being Nat holds (Partial_Sums F) . n is_measurable_on E ) & ( for x being Element of X st x in E holds
F # x is summable ) holds
lim (Partial_Sums F) is_measurable_on E
let S be SigmaField of X; ::_thesis: for E being Element of S
for F being Functional_Sequence of X,COMPLEX st dom (F . 0) = E & F is with_the_same_dom & ( for n being Nat holds (Partial_Sums F) . n is_measurable_on E ) & ( for x being Element of X st x in E holds
F # x is summable ) holds
lim (Partial_Sums F) is_measurable_on E
let E be Element of S; ::_thesis: for F being Functional_Sequence of X,COMPLEX st dom (F . 0) = E & F is with_the_same_dom & ( for n being Nat holds (Partial_Sums F) . n is_measurable_on E ) & ( for x being Element of X st x in E holds
F # x is summable ) holds
lim (Partial_Sums F) is_measurable_on E
let F be Functional_Sequence of X,COMPLEX; ::_thesis: ( dom (F . 0) = E & F is with_the_same_dom & ( for n being Nat holds (Partial_Sums F) . n is_measurable_on E ) & ( for x being Element of X st x in E holds
F # x is summable ) implies lim (Partial_Sums F) is_measurable_on E )
assume that
A1: dom (F . 0) = E and
A2: F is with_the_same_dom and
A3: for n being Nat holds (Partial_Sums F) . n is_measurable_on E and
A4: for x being Element of X st x in E holds
F # x is summable ; ::_thesis: lim (Partial_Sums F) is_measurable_on E
A5: dom ((Im F) . 0) = E by A1, MESFUN7C:def_12;
A6: for x being 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; ::_thesis: ( x in dom ((Partial_Sums F) . 0) implies (Partial_Sums F) # x is convergent )
assume A7: x in dom ((Partial_Sums F) . 0) ; ::_thesis: (Partial_Sums F) # x is convergent
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; ::_thesis: verum
end;
A9: for n being Nat holds (Partial_Sums (Im F)) . n is_measurable_on E
proof
let n be Nat; ::_thesis: (Partial_Sums (Im F)) . n is_measurable_on E
 (Partial_Sums F) . n is_measurable_on E by A3;
then  Im ((Partial_Sums F) . n) is_measurable_on E by MESFUN6C:def_1;
then  (Im (Partial_Sums F)) . n is_measurable_on E by MESFUN7C:24;
hence  (Partial_Sums (Im F)) . n is_measurable_on E by Th29; ::_thesis: verum
end;
A10: for x being Element of X st x in E holds
(Im F) # x is summable
proof
let x be Element of X; ::_thesis: ( x in E implies (Im F) # x is summable )
assume A11: x in E ; ::_thesis: (Im F) # x is summable
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; ::_thesis: verum
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_measurable_on E by A5, A9, A10, Th18;
then A13: lim (Im (Partial_Sums F)) is_measurable_on E by Th29;
A14: for x being Element of X st x in E holds
(Re F) # x is summable
proof
let x be Element of X; ::_thesis: ( x in E implies (Re F) # x is summable )
assume A15: x in E ; ::_thesis: (Re F) # x is summable
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; ::_thesis: verum
end;
A16: for n being Nat holds (Partial_Sums (Re F)) . n is_measurable_on E
proof
let n be Nat; ::_thesis: (Partial_Sums (Re F)) . n is_measurable_on E
 (Partial_Sums F) . n is_measurable_on E by A3;
then  Re ((Partial_Sums F) . n) is_measurable_on E by MESFUN6C:def_1;
then  (Re (Partial_Sums F)) . n is_measurable_on E by MESFUN7C:24;
hence  (Partial_Sums (Re F)) . n is_measurable_on E by Th29; ::_thesis: verum
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_measurable_on E by A13, MESFUNC6:def_1;
 dom ((Re F) . 0) = E by A1, MESFUN7C:def_11;
then  lim (Partial_Sums (Re F)) is_measurable_on E by A12, A16, A14, Th18;
then A19: lim (Re (Partial_Sums F)) is_measurable_on E 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_measurable_on E by A19, MESFUNC6:def_1;
hence  lim (Partial_Sums F) is_measurable_on E by A18, MESFUN6C:def_1; ::_thesis: verum
end;

theorem :: MESFUN9C:40
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for F being Functional_Sequence of X,COMPLEX st ( for n being Nat holds F . n is_integrable_on M ) holds
for m being Nat holds (Partial_Sums F) . m is_integrable_on M
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for F being Functional_Sequence of X,COMPLEX st ( for n being Nat holds F . n is_integrable_on M ) holds
for m being Nat holds (Partial_Sums F) . m is_integrable_on M
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for F being Functional_Sequence of X,COMPLEX st ( for n being Nat holds F . n is_integrable_on M ) holds
for m being Nat holds (Partial_Sums F) . m is_integrable_on M
let M be sigma_Measure of S; ::_thesis: for F being Functional_Sequence of X,COMPLEX st ( for n being Nat holds F . n is_integrable_on M ) holds
for m being Nat holds (Partial_Sums F) . m is_integrable_on M
let F be Functional_Sequence of X,COMPLEX; ::_thesis: ( ( for n being Nat holds F . n is_integrable_on M ) implies for m being Nat holds (Partial_Sums F) . m is_integrable_on M )
assume A1: for n being Nat holds F . n is_integrable_on M ; ::_thesis: for m being Nat holds (Partial_Sums F) . m is_integrable_on M
A2: for n being Nat holds (Im F) . n is_integrable_on M
proof
let n be Nat; ::_thesis: (Im F) . n is_integrable_on M
 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; ::_thesis: verum
end;
A3: for n being Nat holds (Re F) . n is_integrable_on M
proof
let n be Nat; ::_thesis: (Re F) . n is_integrable_on M
 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; ::_thesis: verum
end;
thus  for m being Nat holds (Partial_Sums F) . m is_integrable_on M ::_thesis: verum
proof
let m be Nat; ::_thesis: (Partial_Sums F) . m is_integrable_on M
 (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; ::_thesis: verum
end;
end;

begin


theorem :: MESFUN9C:41
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for A being Element of S st f is_simple_func_in S holds
f is_measurable_on A
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for A being Element of S st f is_simple_func_in S holds
f is_measurable_on A
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,COMPLEX
for A being Element of S st f is_simple_func_in S holds
f is_measurable_on A
let f be PartFunc of X,COMPLEX; ::_thesis: for A being Element of S st f is_simple_func_in S holds
f is_measurable_on A
let A be Element of S; ::_thesis: ( f is_simple_func_in S implies f is_measurable_on A )
assume A1: f is_simple_func_in S ; ::_thesis: f is_measurable_on A
then  Im f is_simple_func_in S by MESFUN7C:43;
then A2: Im f is_measurable_on A by MESFUNC6:50;
 Re f is_simple_func_in S by A1, MESFUN7C:43;
then  Re f is_measurable_on A by MESFUNC6:50;
hence  f is_measurable_on A by A2, MESFUN6C:def_1; ::_thesis: verum
end;

theorem :: MESFUN9C:42
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for A being Element of S st f is_simple_func_in S holds
f | A is_simple_func_in S
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for A being Element of S st f is_simple_func_in S holds
f | A is_simple_func_in S
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,COMPLEX
for A being Element of S st f is_simple_func_in S holds
f | A is_simple_func_in S
let f be PartFunc of X,COMPLEX; ::_thesis: for A being Element of S st f is_simple_func_in S holds
f | A is_simple_func_in S
let A be Element of S; ::_thesis: ( f is_simple_func_in S implies f | A is_simple_func_in S )
assume A1: f is_simple_func_in S ; ::_thesis: f | A 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; ::_thesis: verum
end;

theorem :: MESFUN9C:43
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX st f is_simple_func_in S holds
dom f is Element of S
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,COMPLEX st f is_simple_func_in S holds
dom f is Element of S
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,COMPLEX st f is_simple_func_in S holds
dom f is Element of S
let f be PartFunc of X,COMPLEX; ::_thesis: ( f is_simple_func_in S implies dom f is Element of S )
assume  f is_simple_func_in S ; ::_thesis: dom f is Element of S
then  ex F being Finite_Sep_Sequence of S st
( dom f = union (rng F) & ( for n being Nat
for x, y being Element of X st n in dom F & x in F . n & y in F . n holds
f . x = f . y ) ) by MESFUN7C:def_13;
hence  dom f is Element of S by MESFUNC2:31; ::_thesis: verum
end;

theorem :: MESFUN9C:44
for X being non empty set
for S being SigmaField of X
for f, g being PartFunc of X,COMPLEX st f is_simple_func_in S & g is_simple_func_in S holds
f + g is_simple_func_in S
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f, g being PartFunc of X,COMPLEX st f is_simple_func_in S & g is_simple_func_in S holds
f + g is_simple_func_in S
let S be SigmaField of X; ::_thesis: for f, g being PartFunc of X,COMPLEX st f is_simple_func_in S & g is_simple_func_in S holds
f + g is_simple_func_in S
let f, g be PartFunc of X,COMPLEX; ::_thesis: ( f is_simple_func_in S & g is_simple_func_in S implies f + g is_simple_func_in S )
assume A1: ( f is_simple_func_in S & g is_simple_func_in S ) ; ::_thesis: f + 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  f + g is_simple_func_in S by A2, MESFUN7C:43; ::_thesis: verum
end;

theorem :: MESFUN9C:45
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for c being complex number st f is_simple_func_in S holds
c (#) f is_simple_func_in S
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for c being complex number st f is_simple_func_in S holds
c (#) f is_simple_func_in S
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,COMPLEX
for c being complex number st f is_simple_func_in S holds
c (#) f is_simple_func_in S
let f be PartFunc of X,COMPLEX; ::_thesis: for c being complex number st f is_simple_func_in S holds
c (#) f is_simple_func_in S
let c be complex number ; ::_thesis: ( f is_simple_func_in S implies c (#) f is_simple_func_in S )
assume A1: f is_simple_func_in S ; ::_thesis: c (#) 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  c (#) f is_simple_func_in S by A6, MESFUN7C:43; ::_thesis: verum
end;

begin


theorem Th46: :: MESFUN9C:46
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for F being with_the_same_dom Functional_Sequence of X,ExtREAL
for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) holds
lim F is_integrable_on M
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for F being with_the_same_dom Functional_Sequence of X,ExtREAL
for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) holds
lim F is_integrable_on M
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for E being Element of S
for F being with_the_same_dom Functional_Sequence of X,ExtREAL
for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) holds
lim F is_integrable_on M
let M be sigma_Measure of S; ::_thesis: for E being Element of S
for F being with_the_same_dom Functional_Sequence of X,ExtREAL
for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) holds
lim F is_integrable_on M
let E be Element of S; ::_thesis: for F being with_the_same_dom Functional_Sequence of X,ExtREAL
for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) holds
lim F is_integrable_on M
let F be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) holds
lim F is_integrable_on M
let P be PartFunc of X,ExtREAL; ::_thesis: ( E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) implies lim F is_integrable_on M )
assume that
A1: E = dom (F . 0) and
A2: E = dom P and
A3: for n being Nat holds F . n is_measurable_on E and
A4: P is_integrable_on M and
A5: for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x and
A6: for x being Element of X st x in E holds
F # x is convergent ; ::_thesis: lim F is_integrable_on M
A7: E = dom (lim_sup F) by A1, MESFUNC8:def_8;
A8: for x being Element of X
for k being Nat st x in E holds
( - (P . x) <= (F # x) . k & (F # x) . k <= P . x )
proof
let x be Element of X; ::_thesis: for k being Nat st x in E holds
( - (P . x) <= (F # x) . k & (F # x) . k <= P . x )
let k be Nat; ::_thesis: ( x in E implies ( - (P . x) <= (F # x) . k & (F # x) . k <= P . x ) )
assume A9: x in E ; ::_thesis: ( - (P . x) <= (F # x) . k & (F # x) . k <= P . x )
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 EXTREAL2:12;
hence  ( - (P . x) <= (F # x) . k & (F # x) . k <= P . x ) by MESFUNC5:def_13; ::_thesis: verum
end;
A11: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_sup_F)_holds_
|.((lim_sup_F)_._x).|_<=_P_._x
let x be Element of X; ::_thesis: ( x in dom (lim_sup F) implies |.((lim_sup F) . x).| <= P . x )
assume A12: x in dom (lim_sup F) ; ::_thesis: |.((lim_sup F) . x).| <= P . x
 for k being Nat holds (superior_realsequence (F # x)) . k >= - (P . x)
proof
let k be Nat; ::_thesis: (superior_realsequence (F # x)) . k >= - (P . x)
 k is Element of NAT by ORDINAL1:def_12;
then 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; ::_thesis: verum
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__::_thesis:_for_y_being_ext-real_number_st_y_in_rng_(F_#_x)_holds_
P_._x_>=_y
let y be ext-real number ; ::_thesis: ( y in rng (F # x) implies P . x >= y )
assume  y in rng (F # x) ; ::_thesis: P . x >= y
then  ex k being set st
( k in dom (F # x) & y = (F # x) . k ) by FUNCT_1:def_3;
hence  P . x >= y by A7, A8, A12; ::_thesis: verum
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, EXTREAL2:12; ::_thesis: verum
end;
A16: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_F)_holds_
(lim_F)_._x_=_(lim_sup_F)_._x
let x be Element of X; ::_thesis: ( x in dom (lim F) implies (lim F) . x = (lim_sup F) . x )
assume A17: x in dom (lim F) ; ::_thesis: (lim F) . x = (lim_sup F) . x
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; ::_thesis: verum
end;
A18: lim_sup F is_measurable_on E 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; ::_thesis: verum
end;


theorem Th47: :: MESFUN9C:47
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for F being with_the_same_dom Functional_Sequence of X,REAL
for P being PartFunc of X,REAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) holds
lim F is_integrable_on M
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for F being with_the_same_dom Functional_Sequence of X,REAL
for P being PartFunc of X,REAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) holds
lim F is_integrable_on M
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for E being Element of S
for F being with_the_same_dom Functional_Sequence of X,REAL
for P being PartFunc of X,REAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) holds
lim F is_integrable_on M
let M be sigma_Measure of S; ::_thesis: for E being Element of S
for F being with_the_same_dom Functional_Sequence of X,REAL
for P being PartFunc of X,REAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) holds
lim F is_integrable_on M
let E be Element of S; ::_thesis: for F being with_the_same_dom Functional_Sequence of X,REAL
for P being PartFunc of X,REAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) holds
lim F is_integrable_on M
let F be with_the_same_dom Functional_Sequence of X,REAL; ::_thesis: for P being PartFunc of X,REAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) holds
lim F is_integrable_on M
let P be PartFunc of X,REAL; ::_thesis: ( E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) implies lim F is_integrable_on M )
assume that
A1: ( E = dom (F . 0) & E = dom P ) and
A2: for n being Nat holds F . n is_measurable_on E and
A3: P is_integrable_on M and
A4: for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x and
A5: for x being Element of X st x in E holds
F # x is convergent ; ::_thesis: lim F is_integrable_on M
A6: for n being Nat holds (R_EAL F) . n is_measurable_on E
proof
let n be Nat; ::_thesis: (R_EAL F) . n is_measurable_on E
 F . n is_measurable_on E by A2;
then  R_EAL (F . n) is_measurable_on E by MESFUNC6:def_1;
hence  (R_EAL F) . n is_measurable_on E ; ::_thesis: verum
end;
A7: for x being Element of X st x in E holds
(R_EAL F) # x is convergent
proof
let x be Element of X; ::_thesis: ( x in E implies (R_EAL F) # x is convergent )
assume  x in E ; ::_thesis: (R_EAL F) # x is convergent
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; ::_thesis: verum
end;
A9: for x being Element of X
for n being Nat st x in E holds
|.((R_EAL F) . n).| . x <= (R_EAL P) . x
proof
let x be Element of X; ::_thesis: for n being Nat st x in E holds
|.((R_EAL F) . n).| . x <= (R_EAL P) . x
let n be Nat; ::_thesis: ( x in E implies |.((R_EAL F) . n).| . x <= (R_EAL P) . x )
A10: R_EAL |.(F . n).| = |.(R_EAL (F . n)).| by MESFUNC6:1;
assume  x in E ; ::_thesis: |.((R_EAL F) . n).| . x <= (R_EAL P) . x
hence  |.((R_EAL F) . n).| . x <= (R_EAL P) . x by A4, A10; ::_thesis: verum
end;
 R_EAL P is_integrable_on M by A3, MESFUNC6:def_4;
hence  lim F is_integrable_on M by A1, A6, A9, A7, Th46; ::_thesis: verum
end;

theorem Th48: :: MESFUN9C:48
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for F being with_the_same_dom Functional_Sequence of X,REAL
for P being PartFunc of X,REAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) holds
ex I being Real_Sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for F being with_the_same_dom Functional_Sequence of X,REAL
for P being PartFunc of X,REAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) holds
ex I being Real_Sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for E being Element of S
for F being with_the_same_dom Functional_Sequence of X,REAL
for P being PartFunc of X,REAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) holds
ex I being Real_Sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )
let M be sigma_Measure of S; ::_thesis: for E being Element of S
for F being with_the_same_dom Functional_Sequence of X,REAL
for P being PartFunc of X,REAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) holds
ex I being Real_Sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )
let E be Element of S; ::_thesis: for F being with_the_same_dom Functional_Sequence of X,REAL
for P being PartFunc of X,REAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) holds
ex I being Real_Sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )
let F be with_the_same_dom Functional_Sequence of X,REAL; ::_thesis: for P being PartFunc of X,REAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) holds
ex I being Real_Sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )
let P be PartFunc of X,REAL; ::_thesis: ( E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) implies ex I being Real_Sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) ) )
assume that
A1: E = dom (F . 0) and
A2: E = dom P and
A3: for n being Nat holds F . n is_measurable_on E and
A4: P is_integrable_on M and
A5: for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ; ::_thesis: ex I being Real_Sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )
A6: R_EAL P is_integrable_on M by A4, MESFUNC6:def_4;
A7: for x being Element of X
for n being Nat st x in E holds
|.((R_EAL F) . n).| . x <= (R_EAL P) . x
proof
let x be Element of X; ::_thesis: for n being Nat st x in E holds
|.((R_EAL F) . n).| . x <= (R_EAL P) . x
let n be Nat; ::_thesis: ( x in E implies |.((R_EAL F) . n).| . x <= (R_EAL P) . x )
A8: R_EAL |.(F . n).| = |.(R_EAL (F . n)).| by MESFUNC6:1;
assume  x in E ; ::_thesis: |.((R_EAL F) . n).| . x <= (R_EAL P) . x
hence  |.((R_EAL F) . n).| . x <= (R_EAL P) . x by A5, A8; ::_thesis: verum
end;
A9: for n being Nat holds (R_EAL F) . n is_measurable_on E
proof
let n be Nat; ::_thesis: (R_EAL F) . n is_measurable_on E
 F . n is_measurable_on E by A3;
then  R_EAL (F . n) is_measurable_on E by MESFUNC6:def_1;
hence  (R_EAL F) . n is_measurable_on E ; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_dom_P_holds_
0_<=_P_._x
let x be set ; ::_thesis: ( x in dom P implies 0 <= P . x )
assume A10: x in dom P ; ::_thesis: 0 <= P . x
then  x in dom |.(F . 0).| by A1, A2, VALUED_1:def_11;
then  |.(F . 0).| . x = |.((F . 0) . x).| by VALUED_1:def_11;
then  |.((F . 0) . x).| <= P . x by A2, A5, A10;
hence  0 <= P . x by COMPLEX1:46; ::_thesis: verum
end;
then  P is nonnegative by MESFUNC6:52;
then consider J being ExtREAL_sequence such that
A11: for n being 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 being 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 being Nat holds |.(J . n).| < +infty
proof
let n be Nat; ::_thesis: |.(J . n).| < +infty
A14: ( E = dom ((R_EAL F) . n) & (R_EAL F) . n is_measurable_on E ) 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 being 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; ::_thesis: ( x in dom ((R_EAL F) . n) implies |.(((R_EAL F) . n) . x).| <= (R_EAL P) . x )
assume A16: x in dom ((R_EAL F) . n) ; ::_thesis: |.(((R_EAL F) . n) . x).| <= (R_EAL P) . x
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; ::_thesis: verum
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; ::_thesis: verum
end;
then  for n being Element of NAT st n in dom J holds
|.(J . n).| < +infty ;
then  J is V59() by MESFUNC2:def_1;
then reconsider I = J as Real_Sequence by RINFSUP2:6;
 ( ( for x being 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 being Element of X st x in E holds
F # x is convergent ; ::_thesis: ( J is convergent_to_finite_number & lim J = Integral (M,(lim F)) )
A19: now__::_thesis:_for_x_being_Element_of_X_st_x_in_E_holds_
(R_EAL_F)_#_x_is_convergent
let x be Element of X; ::_thesis: ( x in E implies (R_EAL F) # x is convergent )
assume  x in E ; ::_thesis: (R_EAL F) # x is convergent
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; ::_thesis: verum
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;
now__::_thesis:_(_J_is_convergent_implies_J_is_convergent_to_finite_number_)
assume A22: J is convergent ; ::_thesis: J is convergent_to_finite_number
assume  not J is convergent_to_finite_number ; ::_thesis: contradiction
then  ( J is convergent_to_+infty or J is convergent_to_-infty ) by A22, MESFUNC5:def_11;
hence  contradiction by A12, A19, A21, MESFUNC5:def_12; ::_thesis: verum
end;
hence  ( J is convergent_to_finite_number & lim J = Integral (M,(lim F)) ) by A12, A19; ::_thesis: verum
end;
then A23: ( ( for x being 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 being Nat holds I . n = Integral (M,(F . n)) by A11;
hence  ex I being Real_Sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) ) by A23; ::_thesis: verum
end;

definition
let X be set ;
let F be Functional_Sequence of X,REAL;
attrF is uniformly_bounded  means :Def4: :: MESFUN9C:def 4
 ex K being real number st
for n being Nat
for x being Element of X st x in dom (F . 0) holds
|.((F . n) . x).| <= K;
end;

:: deftheorem Def4 defines uniformly_bounded MESFUN9C:def_4_:_
 for X being set
for F being Functional_Sequence of X,REAL holds
( F is uniformly_bounded iff ex K being real number st
for n being Nat
for x being Element of X st x in dom (F . 0) holds
|.((F . n) . x).| <= K );

theorem Th49: :: MESFUN9C:49
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for F being with_the_same_dom Functional_Sequence of X,REAL st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_measurable_on E ) & F is uniformly_bounded & ( for x being Element of X st x in E holds
F # x is convergent ) holds
( ( for n being Nat holds F . n is_integrable_on M ) & lim F is_integrable_on M & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for F being with_the_same_dom Functional_Sequence of X,REAL st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_measurable_on E ) & F is uniformly_bounded & ( for x being Element of X st x in E holds
F # x is convergent ) holds
( ( for n being Nat holds F . n is_integrable_on M ) & lim F is_integrable_on M & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for E being Element of S
for F being with_the_same_dom Functional_Sequence of X,REAL st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_measurable_on E ) & F is uniformly_bounded & ( for x being Element of X st x in E holds
F # x is convergent ) holds
( ( for n being Nat holds F . n is_integrable_on M ) & lim F is_integrable_on M & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) )
let M be sigma_Measure of S; ::_thesis: for E being Element of S
for F being with_the_same_dom Functional_Sequence of X,REAL st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_measurable_on E ) & F is uniformly_bounded & ( for x being Element of X st x in E holds
F # x is convergent ) holds
( ( for n being Nat holds F . n is_integrable_on M ) & lim F is_integrable_on M & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) )
let E be Element of S; ::_thesis: for F being with_the_same_dom Functional_Sequence of X,REAL st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_measurable_on E ) & F is uniformly_bounded & ( for x being Element of X st x in E holds
F # x is convergent ) holds
( ( for n being Nat holds F . n is_integrable_on M ) & lim F is_integrable_on M & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) )
let F be with_the_same_dom Functional_Sequence of X,REAL; ::_thesis: ( M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_measurable_on E ) & F is uniformly_bounded & ( for x being Element of X st x in E holds
F # x is convergent ) implies ( ( for n being Nat holds F . n is_integrable_on M ) & lim F is_integrable_on M & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) ) )
assume that
A1: ( M . E < +infty & E = dom (F . 0) ) and
A2: for n being Nat holds F . n is_measurable_on E and
A3: F is uniformly_bounded and
A4: for x being Element of X st x in E holds
F # x is convergent ; ::_thesis: ( ( for n being Nat holds F . n is_integrable_on M ) & lim F is_integrable_on M & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) )
consider K being real number  such that
A5: for n being Nat
for x being Element of X st x in dom (F . 0) holds
|.((F . n) . x).| <= K by A3, Def4;
A6: for x being Element of X st x in E holds
(R_EAL F) # x is convergent
proof
let x be Element of X; ::_thesis: ( x in E implies (R_EAL F) # x is convergent )
assume  x in E ; ::_thesis: (R_EAL F) # x is convergent
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; ::_thesis: verum
end;
 for n being Nat
for x being set st x in dom ((R_EAL F) . 0) holds
|.(((R_EAL F) . n) . x).| <= K
proof
let n be Nat; ::_thesis: for x being set st x in dom ((R_EAL F) . 0) holds
|.(((R_EAL F) . n) . x).| <= K
let x be set ; ::_thesis: ( x in dom ((R_EAL F) . 0) implies |.(((R_EAL F) . n) . x).| <= K )
A8: |.((F . n) . x).| = |.(R_EAL ((F . n) . x)).| by MESFUNC6:43;
assume  x in dom ((R_EAL F) . 0) ; ::_thesis: |.(((R_EAL F) . n) . x).| <= K
hence  |.(((R_EAL F) . n) . x).| <= K by A5, A8; ::_thesis: verum
end;
then A9: R_EAL F is uniformly_bounded by MESFUN10:def_1;
A10: for n being Nat holds (R_EAL F) . n is_measurable_on E
proof
let n be Nat; ::_thesis: (R_EAL F) . n is_measurable_on E
 F . n is_measurable_on E by A2;
then  R_EAL (F . n) is_measurable_on E by MESFUNC6:def_1;
hence  (R_EAL F) . n is_measurable_on E ; ::_thesis: verum
end;
then consider I being ExtREAL_sequence such that
A11: for n being 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;
A13: for n being Nat holds F . n is_integrable_on M
proof
let n be Nat; ::_thesis: F . n is_integrable_on M
 R_EAL (F . n) is_integrable_on M by A1, A10, A9, A6, MESFUN10:19;
hence  F . n is_integrable_on M by MESFUNC6:def_4; ::_thesis: verum
end;
 for n being Nat holds I . n = Integral (M,(F . n)) by A11;
hence  ( ( for n being Nat holds F . n is_integrable_on M ) & lim F is_integrable_on M & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) ) by A1, A10, A9, A6, A12, A13, MESFUN10:19; ::_thesis: verum
end;

definition
let X be set ;
let F be Functional_Sequence of X,REAL;
let f be PartFunc of X,REAL;
predF is_uniformly_convergent_to f means :Def5: :: MESFUN9C:def 5
( F is with_the_same_dom & dom (F . 0) = dom f & ( for e being real number st e > 0 holds
ex N being Nat st
for n being Nat
for x being Element of X st n >= N & x in dom (F . 0) holds
|.(((F . n) . x) - (f . x)).| < e ) );
end;

:: deftheorem Def5 defines is_uniformly_convergent_to MESFUN9C:def_5_:_
 for X being set
for F being Functional_Sequence of X,REAL
for f being PartFunc of X,REAL holds
( F is_uniformly_convergent_to f iff ( F is with_the_same_dom & dom (F . 0) = dom f & ( for e being real number st e > 0 holds
ex N being Nat st
for n being Nat
for x being Element of X st n >= N & x in dom (F . 0) holds
|.(((F . n) . x) - (f . x)).| < e ) ) );

theorem Th50: :: MESFUN9C:50
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for F being with_the_same_dom Functional_Sequence of X,REAL
for f being PartFunc of X,REAL st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f holds
( f is_integrable_on M & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,f) ) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for F being with_the_same_dom Functional_Sequence of X,REAL
for f being PartFunc of X,REAL st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f holds
( f is_integrable_on M & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,f) ) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for E being Element of S
for F being with_the_same_dom Functional_Sequence of X,REAL
for f being PartFunc of X,REAL st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f holds
( f is_integrable_on M & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,f) ) )
let M be sigma_Measure of S; ::_thesis: for E being Element of S
for F being with_the_same_dom Functional_Sequence of X,REAL
for f being PartFunc of X,REAL st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f holds
( f is_integrable_on M & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,f) ) )
let E be Element of S; ::_thesis: for F being with_the_same_dom Functional_Sequence of X,REAL
for f being PartFunc of X,REAL st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f holds
( f is_integrable_on M & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,f) ) )
let F be with_the_same_dom Functional_Sequence of X,REAL; ::_thesis: for f being PartFunc of X,REAL st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f holds
( f is_integrable_on M & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,f) ) )
let f be PartFunc of X,REAL; ::_thesis: ( M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f implies ( f is_integrable_on M & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,f) ) ) )
assume that
A1: ( M . E < +infty & E = dom (F . 0) ) and
A2: for n being Nat holds F . n is_integrable_on M and
A3: F is_uniformly_convergent_to f ; ::_thesis: ( f is_integrable_on M & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,f) ) )
A4: for n being Nat holds (R_EAL F) . n is_integrable_on M
proof
let n be Nat; ::_thesis: (R_EAL F) . n is_integrable_on M
 F . n is_integrable_on M by A2;
then  R_EAL (F . n) is_integrable_on M by MESFUNC6:def_4;
hence  (R_EAL F) . n is_integrable_on M ; ::_thesis: verum
end;
A5: for e being real number st e > 0 holds
ex N being Nat st
for n being Nat
for x being 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 number ; ::_thesis: ( e > 0 implies ex N being Nat st
for n being Nat
for x being set st n >= N & x in dom ((R_EAL F) . 0) holds
|.((((R_EAL F) . n) . x) - ((R_EAL f) . x)).| < e )
assume  e > 0 ; ::_thesis: ex N being Nat st
for n being Nat
for x being set st n >= N & x in dom ((R_EAL F) . 0) holds
|.((((R_EAL F) . n) . x) - ((R_EAL f) . x)).| < e
then consider N being Nat such that
A6: for n being Nat
for x being Element of X st n >= N & x in dom (F . 0) holds
|.(((F . n) . x) - (f . x)).| < e by A3, Def5;
now__::_thesis:_for_n_being_Nat
for_x_being_set_st_n_>=_N_&_x_in_dom_((R_EAL_F)_._0)_holds_
|.((((R_EAL_F)_._n)_._x)_-_((R_EAL_f)_._x)).|_<_e
let n be Nat; ::_thesis: for x being set st n >= N & x in dom ((R_EAL F) . 0) holds
|.((((R_EAL F) . n) . x) - ((R_EAL f) . x)).| < e
let x be set ; ::_thesis: ( n >= N & x in dom ((R_EAL F) . 0) implies |.((((R_EAL F) . n) . x) - ((R_EAL f) . x)).| < e )
assume  ( n >= N & x in dom ((R_EAL F) . 0) ) ; ::_thesis: |.((((R_EAL F) . n) . x) - ((R_EAL f) . x)).| < e
then A7: |.(((F . n) . x) - (f . x)).| < e by A6;
 |.(((F . n) . x) - (f . x)).| = |.(R_EAL (((F . n) . x) - (f . x))).| by MESFUNC6:43;
hence  |.((((R_EAL F) . n) . x) - ((R_EAL f) . x)).| < e by A7, SUPINF_2:3; ::_thesis: verum
end;
hence  ex N being Nat st
for n being Nat
for x being set st n >= N & x in dom ((R_EAL F) . 0) holds
|.((((R_EAL F) . n) . x) - ((R_EAL f) . x)).| < e ; ::_thesis: verum
end;
 dom ((R_EAL F) . 0) = dom (R_EAL f) by A3, Def5;
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 being ExtREAL_sequence such that
A10: for n being 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 being Nat holds I . n = Integral (M,(F . n)) by A10;
hence  ( f is_integrable_on M & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,f) ) ) by A9, A11, MESFUNC6:def_4; ::_thesis: verum
end;


theorem Th51: :: MESFUN9C:51
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for P being PartFunc of X,REAL
for F being with_the_same_dom Functional_Sequence of X,COMPLEX st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) holds
lim F is_integrable_on M
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for P being PartFunc of X,REAL
for F being with_the_same_dom Functional_Sequence of X,COMPLEX st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) holds
lim F is_integrable_on M
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for E being Element of S
for P being PartFunc of X,REAL
for F being with_the_same_dom Functional_Sequence of X,COMPLEX st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) holds
lim F is_integrable_on M
let M be sigma_Measure of S; ::_thesis: for E being Element of S
for P being PartFunc of X,REAL
for F being with_the_same_dom Functional_Sequence of X,COMPLEX st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) holds
lim F is_integrable_on M
let E be Element of S; ::_thesis: for P being PartFunc of X,REAL
for F being with_the_same_dom Functional_Sequence of X,COMPLEX st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) holds
lim F is_integrable_on M
let P be PartFunc of X,REAL; ::_thesis: for F being with_the_same_dom Functional_Sequence of X,COMPLEX st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) holds
lim F is_integrable_on M
let F be with_the_same_dom Functional_Sequence of X,COMPLEX; ::_thesis: ( E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) implies lim F is_integrable_on M )
assume that
A1: E = dom (F . 0) and
A2: E = dom P and
A3: for n being Nat holds F . n is_measurable_on E and
A4: P is_integrable_on M and
A5: for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x and
A6: for x being Element of X st x in E holds
F # x is convergent ; ::_thesis: lim F is_integrable_on M
A7: for n being Nat holds
( (Re F) . n is_measurable_on E & (Im F) . n is_measurable_on E ) by A3, Lm2;
 for x being Element of X
for n being 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; ::_thesis: for n being Nat st x in E holds
( |.((Re F) . n).| . x <= P . x & |.((Im F) . n).| . x <= P . x )
let n be Nat; ::_thesis: ( x in E implies ( |.((Re F) . n).| . x <= P . x & |.((Im F) . n).| . x <= P . x ) )
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).| <= |.((F # x) . n).| by COMSEQ_3:13;
 Im ((F # x) . n1) = (Im (F # x)) . n1 by COMSEQ_3:def_6;
then A9: |.((Im (F # x)) . n).| <= |.((F # x) . n).| by COMSEQ_3:13;
assume A10: x in E ; ::_thesis: ( |.((Re F) . n).| . x <= P . x & |.((Im F) . n).| . x <= P . x )
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).| <= P . x by A11, A9, XXREAL_0:2;
then A12: |.(((Im F) . n1) . x).| <= P . x by SEQFUNC:def_10;
 (Re F) # x = Re (F # x) by A1, A10, MESFUN7C:23;
then  |.(((Re F) # x) . n1).| <= P . x by A11, A8, XXREAL_0:2;
then  |.(((Re F) . n1) . x).| <= P . x by SEQFUNC:def_10;
hence  ( |.((Re F) . n).| . x <= P . x & |.((Im F) . n).| . x <= P . x ) by A12, VALUED_1:18; ::_thesis: verum
end;
then A13: for x being Element of X
for n being 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 being 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; ::_thesis: ( x in E implies ( (Re F) # x is convergent & (Im F) # x is convergent ) )
assume A15: x in E ; ::_thesis: ( (Re F) # x is convergent & (Im F) # x is convergent )
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; ::_thesis: verum
end;
then A16: for x being 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 by MESFUNC6:def_4;
A18: for x being 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 by MESFUNC6:def_4;
hence  lim F is_integrable_on M by A17, MESFUN6C:def_2; ::_thesis: verum
end;

theorem :: MESFUN9C:52
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for P being PartFunc of X,REAL
for F being with_the_same_dom Functional_Sequence of X,COMPLEX st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) holds
ex I being Complex_Sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for P being PartFunc of X,REAL
for F being with_the_same_dom Functional_Sequence of X,COMPLEX st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) holds
ex I being Complex_Sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for E being Element of S
for P being PartFunc of X,REAL
for F being with_the_same_dom Functional_Sequence of X,COMPLEX st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) holds
ex I being Complex_Sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )
let M be sigma_Measure of S; ::_thesis: for E being Element of S
for P being PartFunc of X,REAL
for F being with_the_same_dom Functional_Sequence of X,COMPLEX st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) holds
ex I being Complex_Sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )
let E be Element of S; ::_thesis: for P being PartFunc of X,REAL
for F being with_the_same_dom Functional_Sequence of X,COMPLEX st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) holds
ex I being Complex_Sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )
let P be PartFunc of X,REAL; ::_thesis: for F being with_the_same_dom Functional_Sequence of X,COMPLEX st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) holds
ex I being Complex_Sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )
let F be with_the_same_dom Functional_Sequence of X,COMPLEX; ::_thesis: ( E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) implies ex I being Complex_Sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) ) )
assume that
A1: E = dom (F . 0) and
A2: E = dom P and
A3: for n being Nat holds F . n is_measurable_on E and
A4: P is_integrable_on M and
A5: for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ; ::_thesis: ex I being Complex_Sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )
A6: E = dom ((Re F) . 0) by A1, MESFUN7C:def_11;
A7: for n being Nat holds
( (Re F) . n is_measurable_on E & (Im F) . n is_measurable_on E ) by A3, Lm2;
A8: for x being Element of X
for n being 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; ::_thesis: for n being Nat st x in E holds
( |.((Re F) . n).| . x <= P . x & |.((Im F) . n).| . x <= P . x )
let n be Nat; ::_thesis: ( x in E implies ( |.((Re F) . n).| . x <= P . x & |.((Im F) . n).| . x <= P . x ) )
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).| <= |.((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).| <= |.((F # x) . n).| by COMSEQ_3:13;
assume A11: x in E ; ::_thesis: ( |.((Re F) . n).| . x <= P . x & |.((Im F) . n).| . x <= P . x )
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).| <= P . x by A12, A10, XXREAL_0:2;
 (Re F) # x = Re (F # x) by A1, A11, MESFUN7C:23;
then  |.(((Re F) # x) . n).| <= P . x by A12, A9, XXREAL_0:2;
then A14: |.(((Re F) . n) . x).| <= P . x by A13, SEQFUNC:def_10;
 |.(((Im F) . n) . x).| <= 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; ::_thesis: verum
end;
then  for x being Element of X
for n being Nat st x in E holds
|.((Re F) . n).| . x <= P . x ;
then consider A being Real_Sequence such that
A15: for n being Nat holds A . n = Integral (M,((Re F) . n)) and
A16: ( ( for x being 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 S1[ Element of NAT , set ] means $2 = Integral (M,(F . $1));
A17: for n being Element of NAT ex y being Element of COMPLEX st S1[n,y]
proof
let n be Element of NAT ; ::_thesis: ex y being Element of COMPLEX st S1[n,y]
 Integral (M,(F . n)) is Element of COMPLEX by XCMPLX_0:def_2;
hence  ex y being Element of COMPLEX st S1[n,y] ; ::_thesis: verum
end;
consider I being Function of NAT,COMPLEX such that
A18: for n being Element of NAT holds S1[n,I . n] from FUNCT_2:sch_3(A17);
reconsider I = I as Complex_Sequence ;
A19: E = dom ((Im F) . 0) by A1, MESFUN7C:def_12;
 for x being Element of X
for n being Nat st x in E holds
|.((Im F) . n).| . x <= P . x by A8;
then consider B being Real_Sequence such that
A20: for n being Nat holds B . n = Integral (M,((Im F) . n)) and
A21: ( ( for x being 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 being Nat holds
( (Re F) . n is_integrable_on M & (Im F) . n is_integrable_on M )
proof
let n be Nat; ::_thesis: ( (Re F) . n is_integrable_on M & (Im F) . n is_integrable_on M )
A23: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_((Re_F)_._n)_holds_
|.(((Re_F)_._n)_._x).|_<=_P_._x
let x be Element of X; ::_thesis: ( x in dom ((Re F) . n) implies |.(((Re F) . n) . x).| <= P . x )
assume  x in dom ((Re F) . n) ; ::_thesis: |.(((Re F) . n) . x).| <= P . x
then  x in E by A6, MESFUNC8:def_2;
then  |.((Re F) . n).| . x <= P . x by A8;
hence  |.(((Re F) . n) . x).| <= P . x by VALUED_1:18; ::_thesis: verum
end;
A24: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_((Im_F)_._n)_holds_
|.(((Im_F)_._n)_._x).|_<=_P_._x
let x be Element of X; ::_thesis: ( x in dom ((Im F) . n) implies |.(((Im F) . n) . x).| <= P . x )
assume  x in dom ((Im F) . n) ; ::_thesis: |.(((Im F) . n) . x).| <= P . x
then  x in E by A19, MESFUNC8:def_2;
then  |.((Im F) . n).| . x <= P . x by A8;
hence  |.(((Im F) . n) . x).| <= P . x by VALUED_1:18; ::_thesis: verum
end;
A25: ( (Re F) . n is_measurable_on E & (Im F) . n is_measurable_on E ) 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; ::_thesis: verum
end;
A26: now__::_thesis:_for_n1_being_set_st_n1_in_NAT_holds_
(_(Re_I)_._n1_=_A_._n1_&_(Im_I)_._n1_=_B_._n1_)
let n1 be set ; ::_thesis: ( n1 in NAT implies ( (Re I) . n1 = A . n1 & (Im I) . n1 = B . n1 ) )
assume  n1 in NAT ; ::_thesis: ( (Re I) . n1 = A . n1 & (Im I) . n1 = B . n1 )
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 being 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; ::_thesis: verum
end;
then  for x being set st x in NAT holds
(Re I) . x = A . x ;
then A33: Re I = A by FUNCT_2:12;
take  I ; ::_thesis: ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )
hereby  ::_thesis: ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) )
let n be Nat; ::_thesis: I . n = Integral (M,(F . n))
 n is Element of NAT by ORDINAL1:def_12;
hence  I . n = Integral (M,(F . n)) by A18; ::_thesis: verum
end;
 for x being set st x in NAT holds
(Im I) . x = B . x by A26;
then A34: Im I = B by FUNCT_2:12;
hereby  ::_thesis: verum
assume A35: for x being Element of X st x in E holds
F # x is convergent ; ::_thesis: ( I is convergent & lim I = Integral (M,(lim F)) )
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__::_thesis:_for_x_being_Element_of_X_st_x_in_E_holds_
(_(Re_F)_#_x_is_convergent_&_(Im_F)_#_x_is_convergent_)
let x be Element of X; ::_thesis: ( x in E implies ( (Re F) # x is convergent & (Im F) # x is convergent ) )
assume A39: x in E ; ::_thesis: ( (Re F) # x is convergent & (Im F) # x is convergent )
 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; ::_thesis: verum
end;
hence  I is convergent by A16, A21, A33, A34, COMSEQ_3:42; ::_thesis: lim I = Integral (M,(lim F))
 for n being Element of 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; ::_thesis: verum
end;
end;

definition
let X be set ;
let F be Functional_Sequence of X,COMPLEX;
attrF is uniformly_bounded  means :Def6: :: MESFUN9C:def 6
 ex K being real number st
for n being Nat
for x being Element of X st x in dom (F . 0) holds
|.((F . n) . x).| <= K;
end;

:: deftheorem Def6 defines uniformly_bounded MESFUN9C:def_6_:_
 for X being set
for F being Functional_Sequence of X,COMPLEX holds
( F is uniformly_bounded iff ex K being real number st
for n being Nat
for x being Element of X st x in dom (F . 0) holds
|.((F . n) . x).| <= K );

theorem :: MESFUN9C:53
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for F being with_the_same_dom Functional_Sequence of X,COMPLEX st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_measurable_on E ) & F is uniformly_bounded & ( for x being Element of X st x in E holds
F # x is convergent ) holds
( ( for n being Nat holds F . n is_integrable_on M ) & lim F is_integrable_on M & ex I being Complex_Sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for F being with_the_same_dom Functional_Sequence of X,COMPLEX st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_measurable_on E ) & F is uniformly_bounded & ( for x being Element of X st x in E holds
F # x is convergent ) holds
( ( for n being Nat holds F . n is_integrable_on M ) & lim F is_integrable_on M & ex I being Complex_Sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for E being Element of S
for F being with_the_same_dom Functional_Sequence of X,COMPLEX st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_measurable_on E ) & F is uniformly_bounded & ( for x being Element of X st x in E holds
F # x is convergent ) holds
( ( for n being Nat holds F . n is_integrable_on M ) & lim F is_integrable_on M & ex I being Complex_Sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) )
let M be sigma_Measure of S; ::_thesis: for E being Element of S
for F being with_the_same_dom Functional_Sequence of X,COMPLEX st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_measurable_on E ) & F is uniformly_bounded & ( for x being Element of X st x in E holds
F # x is convergent ) holds
( ( for n being Nat holds F . n is_integrable_on M ) & lim F is_integrable_on M & ex I being Complex_Sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) )
let E be Element of S; ::_thesis: for F being with_the_same_dom Functional_Sequence of X,COMPLEX st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_measurable_on E ) & F is uniformly_bounded & ( for x being Element of X st x in E holds
F # x is convergent ) holds
( ( for n being Nat holds F . n is_integrable_on M ) & lim F is_integrable_on M & ex I being Complex_Sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) )
let F be with_the_same_dom Functional_Sequence of X,COMPLEX; ::_thesis: ( M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_measurable_on E ) & F is uniformly_bounded & ( for x being Element of X st x in E holds
F # x is convergent ) implies ( ( for n being Nat holds F . n is_integrable_on M ) & lim F is_integrable_on M & ex I being Complex_Sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) ) )
assume that
A1: M . E < +infty and
A2: E = dom (F . 0) and
A3: for n being Nat holds F . n is_measurable_on E and
A4: F is uniformly_bounded and
A5: for x being Element of X st x in E holds
F # x is convergent ; ::_thesis: ( ( for n being Nat holds F . n is_integrable_on M ) & lim F is_integrable_on M & ex I being Complex_Sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) )
consider K being real number  such that
A6: for n being Nat
for x being Element of X st x in dom (F . 0) holds
|.((F . n) . x).| <= K by A4, Def6;
A7: for x being Element of X st x in E holds
(Re F) # x is convergent
proof
let x be Element of X; ::_thesis: ( x in E implies (Re F) # x is convergent )
assume A8: x in E ; ::_thesis: (Re F) # x is convergent
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; ::_thesis: verum
end;
 for n being Nat
for x being Element of X st x in dom ((Im F) . 0) holds
|.(((Im F) . n) . x).| <= K
proof
let n be Nat; ::_thesis: for x being Element of X st x in dom ((Im F) . 0) holds
|.(((Im F) . n) . x).| <= K
let x be Element of X; ::_thesis: ( x in dom ((Im F) . 0) implies |.(((Im F) . n) . x).| <= K )
assume  x in dom ((Im F) . 0) ; ::_thesis: |.(((Im F) . n) . x).| <= K
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;
A11: n is Element of NAT by ORDINAL1:def_12;
then  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).| <= |.((F # x) . n).| by COMSEQ_3:13;
then  |.(((Im F) # x) . n).| <= K by A10, XXREAL_0:2;
hence  |.(((Im F) . n) . x).| <= K by A11, SEQFUNC:def_10; ::_thesis: verum
end;
then A12: Im F is uniformly_bounded by Def4;
A13: for x being Element of X st x in E holds
(Im F) # x is convergent
proof
let x be Element of X; ::_thesis: ( x in E implies (Im F) # x is convergent )
assume A14: x in E ; ::_thesis: (Im F) # x is convergent
then  F # x is convergent Complex_Sequence by A5;
then  Im (F # x) is convergent ;
hence  (Im F) # x is convergent by A2, A14, MESFUN7C:23; ::_thesis: verum
end;
defpred S1[ Element of NAT , set ] means $2 = Integral (M,(F . $1));
A15: for n being Element of NAT ex y being Element of COMPLEX st S1[n,y]
proof
let n be Element of NAT ; ::_thesis: ex y being Element of COMPLEX st S1[n,y]
take  Integral (M,(F . n)) ; ::_thesis: ( Integral (M,(F . n)) is Element of COMPLEX & S1[n, Integral (M,(F . n))] )
thus  ( Integral (M,(F . n)) is Element of COMPLEX & S1[n, Integral (M,(F . n))] ) by XCMPLX_0:def_2; ::_thesis: verum
end;
consider I being Function of NAT,COMPLEX such that
A16: for n being Element of NAT holds S1[n,I . n] from FUNCT_2:sch_3(A15);
reconsider I = I as Complex_Sequence ;
A17: for n being Nat holds
( (Re F) . n is_measurable_on E & (Im F) . n is_measurable_on E ) by A3, Lm2;
 for n being Nat
for x being Element of X st x in dom ((Re F) . 0) holds
|.(((Re F) . n) . x).| <= K
proof
let n be Nat; ::_thesis: for x being Element of X st x in dom ((Re F) . 0) holds
|.(((Re F) . n) . x).| <= K
let x be Element of X; ::_thesis: ( x in dom ((Re F) . 0) implies |.(((Re F) . n) . x).| <= K )
assume  x in dom ((Re F) . 0) ; ::_thesis: |.(((Re F) . n) . x).| <= K
then A18: x in E by A2, MESFUN7C:def_11;
then  |.((F . n) . x).| <= K by A2, A6;
then A19: |.((F # x) . n).| <= K by MESFUN7C:def_9;
A20: n is Element of NAT by ORDINAL1:def_12;
then  Re ((F # x) . n) = (Re (F # x)) . n by COMSEQ_3:def_5;
then  Re ((F # x) . n) = ((Re F) # x) . n by A2, A18, MESFUN7C:23;
then  |.(((Re F) # x) . n).| <= |.((F # x) . n).| by COMSEQ_3:13;
then  |.(((Re F) # x) . n).| <= K by A19, XXREAL_0:2;
hence  |.(((Re F) . n) . x).| <= K by A20, SEQFUNC:def_10; ::_thesis: verum
end;
then A21: Re F is uniformly_bounded by Def4;
A22: E = dom ((Im F) . 0) by A2, MESFUN7C:def_12;
then consider B being ExtREAL_sequence such that
A23: for n being Nat holds B . n = Integral (M,((Im F) . n)) and
A24: B is convergent and
A25: lim B = Integral (M,(lim (Im F))) by A1, A17, A13, A12, Th49;
A26: lim (Im F) is_integrable_on M by A1, A22, A17, A13, A12, Th49;
then  R_EAL (Im (lim F)) is_integrable_on M by A2, A5, MESFUN7C:25;
then A27: Im (lim F) is_integrable_on M by MESFUNC6:def_4;
A28: E = dom ((Re F) . 0) by A2, MESFUN7C:def_11;
then consider A being ExtREAL_sequence such that
A29: for n being Nat holds A . n = Integral (M,((Re F) . n)) and
A30: A is convergent and
A31: lim A = Integral (M,(lim (Re F))) by A1, A17, A7, A21, Th49;
thus A32: for n being Nat holds F . n is_integrable_on M ::_thesis: ( lim F is_integrable_on M & ex I being Complex_Sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) )
proof
let n be Nat; ::_thesis: F . n is_integrable_on M
 (Im F) . n = Im (F . n) by MESFUN7C:24;
then A33: Im (F . n) is_integrable_on M by A1, A22, A17, A13, A12, Th49;
 (Re F) . n = Re (F . n) by MESFUN7C:24;
then  Re (F . n) is_integrable_on M by A1, A28, A17, A7, A21, Th49;
hence  F . n is_integrable_on M by A33, MESFUN6C:def_2; ::_thesis: verum
end;
A34: for n1 being 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 ; ::_thesis: ( n1 in NAT implies ( (R_EAL (Re I)) . n1 = A . n1 & (R_EAL (Im I)) . n1 = B . n1 ) )
assume  n1 in NAT ; ::_thesis: ( (R_EAL (Re I)) . n1 = A . n1 & (R_EAL (Im I)) . n1 = B . n1 )
then reconsider n = n1 as Element of NAT ;
A35: I . n1 = Integral (M,(F . n)) by A16;
 F . n is_integrable_on M by A32;
then consider RF, IF being Real such that
A36: RF = Integral (M,(Re (F . n))) and
A37: IF = Integral (M,(Im (F . n))) and
A38: 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 A38, A35, COMPLEX1:12, MESFUN7C:24;
hence  (R_EAL (Re I)) . n1 = A . n1 by A29, A36; ::_thesis: (R_EAL (Im I)) . n1 = B . n1
 (Im I) . n = Im (I . n) by COMSEQ_3:def_6;
then  ( (Im F) . n = Im (F . n) & (Im I) . n1 = IF ) by A38, A35, COMPLEX1:12, MESFUN7C:24;
hence  (R_EAL (Im I)) . n1 = B . n1 by A23, A37; ::_thesis: verum
end;
then  for n1 being set st n1 in NAT holds
(R_EAL (Im I)) . n1 = B . n1 ;
then A39: Im I = B by FUNCT_2:12;
A40: ( -infty < Integral (M,(lim (Im F))) & Integral (M,(lim (Im F))) < +infty ) by A26, MESFUNC5:96;
A41: now__::_thesis:_(_B_is_convergent_implies_B_is_convergent_to_finite_number_)
assume A42: B is convergent ; ::_thesis: B is convergent_to_finite_number
assume  not B is convergent_to_finite_number ; ::_thesis: contradiction
then  ( B is convergent_to_+infty or B is convergent_to_-infty ) by A42, MESFUNC5:def_11;
hence  contradiction by A24, A25, A40, MESFUNC5:def_12; ::_thesis: verum
end;
then A43: lim (Im I) = Integral (M,(lim (Im F))) by A24, A25, A39, RINFSUP2:15;
A44: Im I is convergent by A24, A39, A41, RINFSUP2:15;
A45: lim (Re F) is_integrable_on M by A1, A28, A17, A7, A21, Th49;
then  R_EAL (Re (lim F)) is_integrable_on M by A2, A5, MESFUN7C:25;
then  Re (lim F) is_integrable_on M by MESFUNC6:def_4;
hence A46: lim F is_integrable_on M by A27, MESFUN6C:def_2; ::_thesis: ex I being Complex_Sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) )
take  I ; ::_thesis: ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) )
 for n1 being set st n1 in NAT holds
(R_EAL (Re I)) . n1 = A . n1 by A34;
then A47: Re I = A by FUNCT_2:12;
thus  for n being Nat holds I . n = Integral (M,(F . n)) ::_thesis: ( I is convergent & lim I = Integral (M,(lim F)) )
proof
let n be Nat; ::_thesis: I . n = Integral (M,(F . n))
 n is Element of NAT by ORDINAL1:def_12;
then A48: ( (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 A49: (Re I) . n = Integral (M,(Re (F . n))) by A29, A47;
 (Im F) . n = Im (F . n) by MESFUN7C:24;
then A50: (Im I) . n = Integral (M,(Im (F . n))) by A23, A39;
 ( I . n = (Re (I . n)) + ((Im (I . n)) * <i>) & F . n is_integrable_on M ) by A32, COMPLEX1:13;
hence  I . n = Integral (M,(F . n)) by A48, A49, A50, MESFUN6C:def_3; ::_thesis: verum
end;
A51: ( -infty < Integral (M,(lim (Re F))) & Integral (M,(lim (Re F))) < +infty ) by A45, MESFUNC5:96;
A52: now__::_thesis:_(_A_is_convergent_implies_A_is_convergent_to_finite_number_)
assume A53: A is convergent ; ::_thesis: A is convergent_to_finite_number
assume  not A is convergent_to_finite_number ; ::_thesis: contradiction
then  ( A is convergent_to_+infty or A is convergent_to_-infty ) by A53, MESFUNC5:def_11;
hence  contradiction by A30, A31, A51, MESFUNC5:def_12; ::_thesis: verum
end;
then A54: Re I is convergent by A30, A47, RINFSUP2:15;
hence  I is convergent by A44, COMSEQ_3:42; ::_thesis: lim I = Integral (M,(lim F))
 for n being Element of NAT holds
( (Re I) . n = Re (I . n) & (Im I) . n = Im (I . n) ) by COMSEQ_3:def_5, COMSEQ_3:def_6;
then A55: lim I = (lim (Re I)) + ((lim (Im I)) * <i>) by A54, A44, COMSEQ_3:39;
A56: ( 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 A30, A31, A47, A52, RINFSUP2:15;
hence  lim I = Integral (M,(lim F)) by A46, A43, A55, A56, MESFUN6C:def_3; ::_thesis: verum
end;

definition
let X be set ;
let F be Functional_Sequence of X,COMPLEX;
let f be PartFunc of X,COMPLEX;
predF is_uniformly_convergent_to f means :Def7: :: MESFUN9C:def 7
( F is with_the_same_dom & dom (F . 0) = dom f & ( for e being real number st e > 0 holds
ex N being Nat st
for n being Nat
for x being Element of X st n >= N & x in dom (F . 0) holds
|.(((F . n) . x) - (f . x)).| < e ) );
end;

:: deftheorem Def7 defines is_uniformly_convergent_to MESFUN9C:def_7_:_
 for X being set
for F being Functional_Sequence of X,COMPLEX
for f being PartFunc of X,COMPLEX holds
( F is_uniformly_convergent_to f iff ( F is with_the_same_dom & dom (F . 0) = dom f & ( for e being real number st e > 0 holds
ex N being Nat st
for n being Nat
for x being Element of X st n >= N & x in dom (F . 0) holds
|.(((F . n) . x) - (f . x)).| < e ) ) );

theorem :: MESFUN9C:54
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for F being with_the_same_dom Functional_Sequence of X,COMPLEX
for f being PartFunc of X,COMPLEX st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f holds
( f is_integrable_on M & ex I being Complex_Sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,f) ) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for F being with_the_same_dom Functional_Sequence of X,COMPLEX
for f being PartFunc of X,COMPLEX st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f holds
( f is_integrable_on M & ex I being Complex_Sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,f) ) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for E being Element of S
for F being with_the_same_dom Functional_Sequence of X,COMPLEX
for f being PartFunc of X,COMPLEX st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f holds
( f is_integrable_on M & ex I being Complex_Sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,f) ) )
let M be sigma_Measure of S; ::_thesis: for E being Element of S
for F being with_the_same_dom Functional_Sequence of X,COMPLEX
for f being PartFunc of X,COMPLEX st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f holds
( f is_integrable_on M & ex I being Complex_Sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,f) ) )
let E be Element of S; ::_thesis: for F being with_the_same_dom Functional_Sequence of X,COMPLEX
for f being PartFunc of X,COMPLEX st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f holds
( f is_integrable_on M & ex I being Complex_Sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,f) ) )
let F be with_the_same_dom Functional_Sequence of X,COMPLEX; ::_thesis: for f being PartFunc of X,COMPLEX st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f holds
( f is_integrable_on M & ex I being Complex_Sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,f) ) )
let f be PartFunc of X,COMPLEX; ::_thesis: ( M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f implies ( f is_integrable_on M & ex I being Complex_Sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,f) ) ) )
assume that
A1: M . E < +infty and
A2: E = dom (F . 0) and
A3: for n being Nat holds F . n is_integrable_on M and
A4: F is_uniformly_convergent_to f ; ::_thesis: ( f is_integrable_on M & ex I being Complex_Sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,f) ) )
A5: for n being Nat holds (Im F) . n is_integrable_on M
proof
let n be Nat; ::_thesis: (Im F) . n is_integrable_on M
 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; ::_thesis: verum
end;
A6: dom (F . 0) = dom f by A4, Def7;
A7: for e being real number st e > 0 holds
ex N being Nat st
for n being Nat
for x being Element of X st n >= N & x in dom ((Im F) . 0) holds
|.((((Im F) . n) . x) - ((Im f) . x)).| < e
proof
let e be real number ; ::_thesis: ( e > 0 implies ex N being Nat st
for n being Nat
for x being Element of X st n >= N & x in dom ((Im F) . 0) holds
|.((((Im F) . n) . x) - ((Im f) . x)).| < e )
assume  e > 0 ; ::_thesis: ex N being Nat st
for n being Nat
for x being Element of X st n >= N & x in dom ((Im F) . 0) holds
|.((((Im F) . n) . x) - ((Im f) . x)).| < e
then consider N being Nat such that
A8: for n being Nat
for x being Element of X st n >= N & x in dom (F . 0) holds
|.(((F . n) . x) - (f . x)).| < e by A4, Def7;
 for n being Nat
for x being Element of X st n >= N & x in dom ((Im F) . 0) holds
|.((((Im F) . n) . x) - ((Im f) . x)).| < e
proof
let n be Nat; ::_thesis: for x being Element of X st n >= N & x in dom ((Im F) . 0) holds
|.((((Im F) . n) . x) - ((Im f) . x)).| < e
let x be Element of X; ::_thesis: ( n >= N & x in dom ((Im F) . 0) implies |.((((Im F) . n) . x) - ((Im f) . x)).| < e )
assume that
A9: n >= N and
A10: x in dom ((Im F) . 0) ; ::_thesis: |.((((Im F) . n) . x) - ((Im f) . x)).| < e
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;
 ((F # x) . n) - (f . x) is Element of COMPLEX by XCMPLX_0:def_2;
then A14: |.((Im ((F # x) . n)) - (Im (f . x))).| <= |.(((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)).| < e by A12, A14, A15, XXREAL_0:2; ::_thesis: verum
end;
hence  ex N being Nat st
for n being Nat
for x being Element of X st n >= N & x in dom ((Im F) . 0) holds
|.((((Im F) . n) . x) - ((Im f) . x)).| < e ; ::_thesis: verum
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, Def5;
A17: for e being real number st e > 0 holds
ex N being Nat st
for n being Nat
for x being Element of X st n >= N & x in dom ((Re F) . 0) holds
|.((((Re F) . n) . x) - ((Re f) . x)).| < e
proof
let e be real number ; ::_thesis: ( e > 0 implies ex N being Nat st
for n being Nat
for x being Element of X st n >= N & x in dom ((Re F) . 0) holds
|.((((Re F) . n) . x) - ((Re f) . x)).| < e )
assume  e > 0 ; ::_thesis: ex N being Nat st
for n being Nat
for x being Element of X st n >= N & x in dom ((Re F) . 0) holds
|.((((Re F) . n) . x) - ((Re f) . x)).| < e
then consider N being Nat such that
A18: for n being Nat
for x being Element of X st n >= N & x in dom (F . 0) holds
|.(((F . n) . x) - (f . x)).| < e by A4, Def7;
 for n being Nat
for x being Element of X st n >= N & x in dom ((Re F) . 0) holds
|.((((Re F) . n) . x) - ((Re f) . x)).| < e
proof
let n be Nat; ::_thesis: for x being Element of X st n >= N & x in dom ((Re F) . 0) holds
|.((((Re F) . n) . x) - ((Re f) . x)).| < e
let x be Element of X; ::_thesis: ( n >= N & x in dom ((Re F) . 0) implies |.((((Re F) . n) . x) - ((Re f) . x)).| < e )
assume that
A19: n >= N and
A20: x in dom ((Re F) . 0) ; ::_thesis: |.((((Re F) . n) . x) - ((Re f) . x)).| < e
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;
 ((F # x) . n) - (f . x) is Element of COMPLEX by XCMPLX_0:def_2;
then A25: |.((Re ((F # x) . n)) - (Re (f . x))).| <= |.(((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)).| < e by A23, A25, A24, XXREAL_0:2; ::_thesis: verum
end;
hence  ex N being Nat st
for n being Nat
for x being Element of X st n >= N & x in dom ((Re F) . 0) holds
|.((((Re F) . n) . x) - ((Re f) . x)).| < e ; ::_thesis: verum
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, Def5;
defpred S1[ Element of NAT , set ] means $2 = Integral (M,(F . $1));
A27: for n being Element of NAT ex y being Element of COMPLEX st S1[n,y]
proof
let n be Element of NAT ; ::_thesis: ex y being Element of COMPLEX st S1[n,y]
 Integral (M,(F . n)) is Element of COMPLEX by XCMPLX_0:def_2;
hence  ex y being Element of COMPLEX st S1[n,y] ; ::_thesis: verum
end;
consider I being Function of NAT,COMPLEX such that
A28: for n being Element of NAT holds S1[n,I . n] from FUNCT_2:sch_3(A27);
A29: for n being Nat holds (Re F) . n is_integrable_on M
proof
let n be Nat; ::_thesis: (Re F) . n is_integrable_on M
 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; ::_thesis: verum
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 being ExtREAL_sequence such that
A33: for n being 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; ::_thesis: ex I being Complex_Sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,f) )
reconsider I = I as Complex_Sequence ;
consider B being ExtREAL_sequence such that
A38: for n being 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__::_thesis:_for_n1_being_set_st_n1_in_NAT_holds_
(_(R_EAL_(Re_I))_._n1_=_A_._n1_&_(R_EAL_(Im_I))_._n1_=_B_._n1_)
let n1 be set ; ::_thesis: ( n1 in NAT implies ( (R_EAL (Re I)) . n1 = A . n1 & (R_EAL (Im I)) . n1 = B . n1 ) )
assume  n1 in NAT ; ::_thesis: ( (R_EAL (Re I)) . n1 = A . n1 & (R_EAL (Im I)) . n1 = B . n1 )
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 being 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; ::_thesis: verum
end;
then  for x being set st x in NAT holds
(R_EAL (Im I)) . x = B . x ;
then A46: Im I = B by FUNCT_2:12;
A47: ( -infty < Integral (M,(Im f)) & Integral (M,(Im f)) < +infty ) by A31, MESFUNC6:90;
A48: now__::_thesis:_(_B_is_convergent_implies_B_is_convergent_to_finite_number_)
assume A49: B is convergent ; ::_thesis: B is convergent_to_finite_number
assume  not B is convergent_to_finite_number ; ::_thesis: contradiction
then  ( B is convergent_to_+infty or B is convergent_to_-infty ) by A49, MESFUNC5:def_11;
hence  contradiction by A39, A40, A47, MESFUNC5:def_12; ::_thesis: verum
end;
then A50: lim (Im I) = Integral (M,(Im f)) by A39, A40, A46, RINFSUP2:15;
A51: Im I is convergent by A39, A46, A48, RINFSUP2:15;
take  I ; ::_thesis: ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,f) )
 for x being set st x in NAT holds
(R_EAL (Re I)) . x = A . x by A41;
then A52: Re I = A by FUNCT_2:12;
thus  for n being Nat holds I . n = Integral (M,(F . n)) ::_thesis: ( I is convergent & lim I = Integral (M,f) )
proof
let n be Nat; ::_thesis: I . n = Integral (M,(F . n))
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 A53: I . n = ((Re I) . n) + (((Im I) . n) * <i>) by COMPLEX1:13;
 (Re F) . n = Re (F . n) by MESFUN7C:24;
then A54: (Re I) . n = Integral (M,(Re (F . n))) by A33, A52;
 (Im F) . n = Im (F . n) by MESFUN7C:24;
then A55: (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 A53, A54, A55, MESFUN6C:def_3; ::_thesis: verum
end;
A56: ( -infty < Integral (M,(Re f)) & Integral (M,(Re f)) < +infty ) by A36, MESFUNC6:90;
A57: now__::_thesis:_(_A_is_convergent_implies_A_is_convergent_to_finite_number_)
assume A58: A is convergent ; ::_thesis: A is convergent_to_finite_number
assume  not A is convergent_to_finite_number ; ::_thesis: contradiction
then  ( A is convergent_to_+infty or A is convergent_to_-infty ) by A58, MESFUNC5:def_11;
hence  contradiction by A34, A35, A56, MESFUNC5:def_12; ::_thesis: verum
end;
then A59: Re I is convergent by A34, A52, RINFSUP2:15;
hence  I is convergent by A51, COMSEQ_3:42; ::_thesis: lim I = Integral (M,f)
 for n being Element of NAT holds
( (Re I) . n = Re (I . n) & (Im I) . n = Im (I . n) ) by COMSEQ_3:def_5, COMSEQ_3:def_6;
then A60: lim I = (lim (Re I)) + ((lim (Im I)) * <i>) by A59, A51, COMSEQ_3:39;
 lim (Re I) = Integral (M,(Re f)) by A34, A35, A52, A57, RINFSUP2:15;
hence  lim I = Integral (M,f) by A37, A50, A60, MESFUN6C:def_3; ::_thesis: verum
end;