:: Lebesgue's Convergence Theorem of Complex-Valued Function
:: by Keiko Narita , Noboru Endou and Yasunari Shidama
::
:: Received March 17, 2009
:: Copyright (c) 2009-2012 Association of Mizar Users


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
proofend;
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
proofend;
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
proofend;

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
proofend;

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)
proofend;

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
proofend;

theorem Th5: :: MESFUN9C:5
for seq being Real_Sequence holds Partial_Sums (R_EAL seq) = R_EAL (Partial_Sums seq)
proofend;

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
proofend;

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)) ) )
proofend;
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
proofend;
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)
proofend;

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) &amp; m <= n holds
( z in dom ((Partial_Sums F) . m) &amp; z in dom (F . m) )
proofend;

theorem Th9: :: MESFUN9C:9
for X being non empty set
for F being Functional_Sequence of X,REAL holds R_EAL F is additive
proofend;

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  }
proofend;

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)
proofend;

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 &amp; D c= dom (F . 0) &amp; x in D holds
(Partial_Sums (F # x)) . n = ((Partial_Sums F) # x) . n
proofend;

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 &amp; D c= dom (F . 0) &amp; x in D holds
( Partial_Sums (F # x) is convergent iff (Partial_Sums F) # x is convergent )
proofend;

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 &amp; dom f c= dom (F . 0) &amp; x in dom f &amp; f . x = Sum (F # x) holds
f . x = lim ((Partial_Sums F) # x)
proofend;

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
proofend;

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
proofend;

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
proofend;

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 &amp; F is with_the_same_dom &amp; ( for n being Nat holds (Partial_Sums F) . n is_measurable_on E ) &amp; ( for x being Element of X st x in E holds
F # x is summable ) holds
lim (Partial_Sums F) is_measurable_on E
proofend;

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
proofend;

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) &amp; (Im f) | A = Im (f | A) )
proofend;

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 &amp; (Im (F || D)) . n = ((Im F) . n) | D )
proofend;

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
proofend;

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
proofend;

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 &amp; D c= dom (F . 0) &amp; x in D &amp; F # x is convergent holds
(F || D) # x is convergent
proofend;

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 )
proofend;

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 )
proofend;

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 &amp; D = dom (F . 0) &amp; ( for x being Element of X st x in D holds
F # x is convergent ) holds
(lim F) | D = lim (F || D)
proofend;

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 &amp; E c= dom (F . 0) &amp; ( for m being Nat holds F . m is_measurable_on E ) holds
(F || E) . n is_measurable_on E
proofend;

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) &amp; F is with_the_same_dom &amp; ( 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
proofend;

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 &amp; ( 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 &amp; ( for n being Nat holds b1 . (n + 1) = (b1 . n) + (F . (n + 1)) ) )
proofend;
uniqueness
 for b1, b2 being Functional_Sequence of X,COMPLEX st b1 . 0 = F . 0 &amp; ( for n being Nat holds b1 . (n + 1) = (b1 . n) + (F . (n + 1)) ) &amp; b2 . 0 = F . 0 &amp; ( for n being Nat holds b2 . (n + 1) = (b2 . n) + (F . (n + 1)) ) holds
b1 = b2
proofend;
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 &amp; ( 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) &amp; Partial_Sums (Im F) = Im (Partial_Sums F) )
proofend;

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) &amp; m <= n holds
( z in dom ((Partial_Sums F) . m) &amp; z in dom (F . m) )
proofend;

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  }
proofend;

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)
proofend;

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 &amp; D c= dom (F . 0) &amp; x in D holds
(Partial_Sums (F # x)) . n = ((Partial_Sums F) # x) . n
proofend;

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
proofend;

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 &amp; D c= dom (F . 0) &amp; x in D holds
( Partial_Sums (F # x) is convergent iff (Partial_Sums F) # x is convergent )
proofend;

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 &amp; dom f c= dom (F . 0) &amp; x in dom f &amp; F # x is summable &amp; f . x = Sum (F # x) holds
f . x = lim ((Partial_Sums F) # x)
proofend;

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
proofend;

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 &amp; (Im F) . m is_measurable_on E )
proofend;

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
proofend;

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 &amp; F is with_the_same_dom &amp; ( for n being Nat holds (Partial_Sums F) . n is_measurable_on E ) &amp; ( for x being Element of X st x in E holds
F # x is summable ) holds
lim (Partial_Sums F) is_measurable_on E
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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 &amp; g is_simple_func_in S holds
f + g is_simple_func_in S
proofend;

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
proofend;

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) &amp; E = dom P &amp; ( for n being Nat holds F . n is_measurable_on E ) &amp; P is_integrable_on M &amp; ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) &amp; ( for x being Element of X st x in E holds
F # x is convergent ) holds
lim F is_integrable_on M
proofend;

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) &amp; E = dom P &amp; ( for n being Nat holds F . n is_measurable_on E ) &amp; P is_integrable_on M &amp; ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) &amp; ( for x being Element of X st x in E holds
F # x is convergent ) holds
lim F is_integrable_on M
proofend;

:: Lebesgue's Convergence theorem
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) &amp; E = dom P &amp; ( for n being Nat holds F . n is_measurable_on E ) &amp; P is_integrable_on M &amp; ( 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)) ) &amp; ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent &amp; lim I = Integral (M,(lim F)) ) ) )
proofend;

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

:: Lebesgue's Bounded Convergence Theorem
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 &amp; E = dom (F . 0) &amp; ( for n being Nat holds F . n is_measurable_on E ) &amp; F is uniformly_bounded &amp; ( 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 ) &amp; lim F is_integrable_on M &amp; ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) &amp; I is convergent &amp; lim I = Integral (M,(lim F)) ) )
proofend;

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 &amp; dom (F . 0) = dom f &amp; ( 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 &amp; 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 &amp; dom (F . 0) = dom f &amp; ( 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 &amp; 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 &amp; E = dom (F . 0) &amp; ( for n being Nat holds F . n is_integrable_on M ) &amp; F is_uniformly_convergent_to f holds
( f is_integrable_on M &amp; ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) &amp; I is convergent &amp; lim I = Integral (M,f) ) )
proofend;

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) &amp; E = dom P &amp; ( for n being Nat holds F . n is_measurable_on E ) &amp; P is_integrable_on M &amp; ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) &amp; ( for x being Element of X st x in E holds
F # x is convergent ) holds
lim F is_integrable_on M
proofend;

:: Lebesgue's Convergence theorem
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) &amp; E = dom P &amp; ( for n being Nat holds F . n is_measurable_on E ) &amp; P is_integrable_on M &amp; ( 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)) ) &amp; ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent &amp; lim I = Integral (M,(lim F)) ) ) )
proofend;

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

:: Lebesgue's Bounded Convergence Theorem
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 &amp; E = dom (F . 0) &amp; ( for n being Nat holds F . n is_measurable_on E ) &amp; F is uniformly_bounded &amp; ( 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 ) &amp; lim F is_integrable_on M &amp; ex I being Complex_Sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) &amp; I is convergent &amp; lim I = Integral (M,(lim F)) ) )
proofend;

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 &amp; dom (F . 0) = dom f &amp; ( 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 &amp; 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 &amp; dom (F . 0) = dom f &amp; ( 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 &amp; 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 &amp; E = dom (F . 0) &amp; ( for n being Nat holds F . n is_integrable_on M ) &amp; F is_uniformly_convergent_to f holds
( f is_integrable_on M &amp; ex I being Complex_Sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) &amp; I is convergent &amp; lim I = Integral (M,f) ) )
proofend;