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